Show simple item record

dc.contributor.authorNieuwenhuis, Robert Lukas Mario
dc.contributor.authorRubio Gimeno, Alberto
dc.contributor.otherUniversitat Politècnica de Catalunya. Departament de Ciències de la Computació
dc.identifier.citationNieuwenhuis, R.; Rubio, A. First-order completion with ordering constraints: some positive and some negative results. 1991.
dc.description.abstractWe 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.
dc.format.extent14 p.
dc.rightsAttribution-NonCommercial-NoDerivs 3.0 Spain
dc.subjectÀrees temàtiques de la UPC::Informàtica
dc.subject.lcshProgramming languages (Electronic computers)
dc.subject.lcshLogic programming
dc.subject.otherAutomated theorem proving
dc.subject.otherProgramming languages
dc.subject.otherLogic programming
dc.titleFirst-order completion with ordering constraints: some positive and some negative results
dc.typeExternal research report
dc.subject.lemacLlenguatges de programació
dc.subject.lemacProgramació lògica
dc.contributor.groupUniversitat Politècnica de Catalunya. LOGPROG - Lògica i Programació
dc.rights.accessOpen Access
dc.description.versionPostprint (published version)
local.citation.authorNieuwenhuis, R.; Rubio, A.

Files in this item


This item appears in the following Collection(s)

Show simple item record

Attribution-NonCommercial-NoDerivs 3.0 Spain
Except where otherwise noted, content on this work is licensed under a Creative Commons license : Attribution-NonCommercial-NoDerivs 3.0 Spain