hide
Free keywords:
-
Abstract:
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.
