MPI-INF/SWS Research Reports 1991-2017

2. Number - only D2


Killer transformations

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

June 1994, 45 pages.

Status: available - back from printing

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 logics. 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.

  • Attachement: (956 KBytes); MPI-I-94-226.pdf (474 KBytes)

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},