Help Privacy Policy Disclaimer
  Advanced SearchBrowse





Computer support for the development and investigation of logics


Ohlbach,  Hans Jürgen
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (public)

(Any fulltext), 12MB

Supplementary Material (public)
There is no public supplementary material available

Ohlbach, H. J.(1994). Computer support for the development and investigation of logics (MPI-I-94-228). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-B7AD-A
Symbolic reasoning in a logical framework becomes more and more important for computer applications such as Natural Language Processing Systems or Expert Systems. These applications usually need specifically tailored logics. Therefore we are developing methods and algorithms for supporting the designer of an application system, who is usually not a logician, to develop his own application oriented logic. This paper gives an overview about our current state of these investigations. In particular we consider the correspondences between axiomatic and semantic specifications of a logic and the problem of finding one from the other. Correlated with this area are translation methods from the object logic into predicate logic, and methods for optimizing the translation. Other topics are investigations of the expressiveness of a logic and the axiomatizability of semantic conditions. The basic techniques underlying our approach, so called K-transformations and quantifier elimination, are briefly discussed. They are quite general mechanisms for manipulating predicate logic formulae, and the investigation of logics is only one of their applications. For the technical details of the methods and the proofs I refer to the original papers.