First-order completion with ordering constraints: some positive and some negative results
Document typeExternal research report
Rights accessOpen Access
We show by means of counter examples that some well-known results on the completeness of deduction methods with ordering constraints are incorrect. The problem is caused by the fact that the usual lifting lemmata do not hold. In this paper, these problems are overcome by using a different lifting method. We define a completion procedure for ordering constrained first-order clauses with equality, including notions of redundant inferences and clauses, as done in [BG 91] for clauses without constraints. This completion procedure is refutationally complete if the initial set of constrained clauses fulfills a property which we have called pureness. In particular, clauses without constraints are pure. Pureness is preserved during the completion process. Since the constraints generated during completion reduce the search space considerably, our results allow to do very efficient theorem proving in first-order logic with equality. Moreover, complete sets of axioms (canonical sets of rewrite rules in the equational case) can be obtained in more cases.
CitationNieuwenhuis, R.; Rubio, A. First-order completion with ordering constraints: some positive and some negative results. 1991.
Is part ofLSI-91-43