Refutational theorem proving using term-rewriting systems (Q802317)

The paper proposes a new approach to theorem proving in first-order logic based on term-rewriting systems. First, for propositional calculus a canonical term-rewriting system for Boolean algebra is introduced. The key point enabling successful construction of the canonical term- rewriting system (in contrast with all the previous attempts that failed due to the fact that the prime implicant representation of Boolean terms is not unique) consists in choosing exclusive or instead of or. The canonical system for Boolean algebra enables transformation of the first- order calculus into a form of equational logic and to develop several complete strategies (both clausal and nonclausal) for first-order theories based on the Knuth-Bendix completion algorithm. These strategies deal with predicate logic and built-in (equational) theories in a uniform and quite efficient way. Comparison of implementation of a theorem prover based on term-rewriting with other theorem provers based on locking reduction or natural deduction shows that the method proposed is in general much more efficient then the methods based on resolution. Great efficiency and easy modifiability of a theorem prover based on the term-rewriting method makes the method a serious counterpart to resolution and it will probably have significant impact on theorem proving.