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


Killer transformations

Ohlbach, Hans J├╝rgen and Gabbay, Dov M. and Plaisted, David A.

MPI-I-94-226. June 1994, 45 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
This paper deals with methods of faithful transformations between logical systems.
Several methods for developing transformations of logical formulae are defined which eliminate unwanted properties from axiom systems without losing theorems. The elementary examples we present are permutation,
transitivity, equivalence relation properties of predicates and congruence properties of functions.
Various translations between logical systems are shown to be instances of
K-transformations, for example the transition from
relational to functional translation of modal logic into predicate
logic, the transition from axiomatic specifications of logics via
unary provability relations to a binary consequence relations, and the
development of neighbourhood semantics for nonclassical propositional

Furthermore we show how to eliminate self resolving clauses like the
condensed detachment clause, resulting in dramatic improvements of the
performance of automated theorem provers on extremely hard problems.
As by--products we get a method for encoding some axioms in Prolog
which normally would generate loops, and we get a method for
parallelizing some closure computation algorithms.
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-226.pdfMPI-I-94-226.pdfMPI-I-94-226.ps956 KBytes; 474 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 and Gabbay, Dov M. and Plaisted, David A.},
  TITLE = {Killer transformations},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-94-226},
  MONTH = {June},
  YEAR = {1994},
  ISSN = {0946-011X},