Help Privacy Policy Disclaimer
  Advanced SearchBrowse





Killer transformation


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


Gabbay,  Murdoch James
Programming Logics, MPI for Informatics, Max Planck Society;


Plaisted,  David
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

(Any fulltext), 475KB

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

Ohlbach, H. J., Gabbay, M. J., & Plaisted, D.(1994). Killer transformation (MPI-I-94-226). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-B5AB-D
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.