THEOREM-PROVING WITH ORDERING AND EQUALITY CONSTRAINED CLAUSES

Deduction methods for first-order constrained clauses with equality are described within an abstract framework: constraint strategies, consisting of an inference system, a constraint inheritance strategy and redundancy criteria for clauses and inferences. We give simple conditions for such a constraint strategy to be complete (refutationally and in the sense of Knuth-Bendix-like completion). This allows to prove in a uniform way the completeness of several instantiations of the framework with concrete strategies. For example, strategies in which equality constraints are inherited are basic: no inferences are needed on subterms introduced by unifiers of previous inferences. Ordering constraints reduce the search space by inheriting the ordering restrictions of previous inferences and increase the expressive power of the logic.