MPI-I-94-228
Computer support for the development and investigation of logics
Ohlbach, Hans Jürgen
July 1994, 24 pages.
.
Status: available - back from printing
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.
-
MPI-I-94-228.pdf
- Attachement: MPI-I-94-228.ps (708 KBytes); MPI-I-94-228.pdf (11477 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1994-228
BibTeX
@TECHREPORT{Ohlbach94a,
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},
}