Computer Support for the Development and Investigation of Logics
Hans Jürgen Ohlbach · Logic Journal of IGPL · 1996
The development and investigation of application-oriented logics comprises many aspects and problems. For a few of them some computer support is possible which frees the investigator from sometimes quite complex computations. This paper gives an overview about some developments in this area. In particular, we consider the correspondences between axiomatic and semantic specifications of a logic and the problem of finding one from the other by means of automated theorem provers and quantifier elimination algorithms. Other topics adressed in this paper are reasoning in Hilbert systems, the investigation of the expressiveness of a logic and the axiomatizability of semantic conditions. For the technical details of the methods and the proofs I refer to the original papers.