Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Computer support for the development and investigation of logics

Ohlbach, Hans J├╝rgen

MPI-I-94-228. July 1994, 24 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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

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

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

For the technical details of the methods and the proofs I refer to the
original papers.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-94-228.pdfMPI-I-94-228.pdfMPI-I-94-228.ps708 KBytes; 11477 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Ohlbach, Hans J{\"u}rgen},
  TITLE = {Computer support for the development and investigation of logics},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-94-228},
  MONTH = {July},
  YEAR = {1994},
  ISSN = {0946-011X},