An equational approach to theorem proving in first-order predicate calculus

Abstract

A new approach for proving theorems in first-order predicate calculus is developed based on term rewriting and polynomial simplification methods. A formula is translated into an equivalent set of formulae expressed in terms of 'true', 'false', 'exclusive-or', and 'and' by analyzing the semantics of its top-level operator. In this representation, formulae are polynomials over atomic formulae with 'and' as multiplication and 'exclusive-or' as addition, and they can be manipulated just like polynomials using familiar rules of multiplication and addition. Polynomials representing a formula are converted into rewrite rules which are used to simplify polynomials. New rules are generated by overlapping polynomials using a critical-pair completion procedure closely related to the Knuth- Bendix procedure. This process is repeated until a contradiction is reached or it is no longer possible to generate new rules. It is shown that resolution is subsumed by this method.