Elsevier

Journal of Symbolic Computation

Volume 11, Issues 1–2, January–February 1991, Pages 21-49
Journal of Symbolic Computation

Theorem-proving with resolution and superposition*

https://doi.org/10.1016/S0747-7171(08)80131-9Get rights and content
Under an Elsevier user license
open archive

Abstract

We present a refutationally complete set of inference rules for first-order logic with equality. Except for x = x, no equality axioms are needed. Equalities are oriented by a well-founded ordering and can be used safely for demodulation without losing completeness. When restricted to equational logic, this strategy reduces to a Knuth-Bendix procedure.

Cited by (0)

*

A preliminary version of the results in this paper has been presented at the International Conference on Fifth Generation Computer Systems (Tokyo 1988).