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 Ionger possible to generate new rules. It is shown that resolution is subsumed by this method .