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.pdf||956 KBytes; 474 KBytes|
|Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView|