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. Basic superposition is complete. 1991.
dc.description.abstractWe define a formalism of equality constraints and use it to prove the completeness of what we have called basic superposition: a restricted form of superposition in which only the subterms not originated in previous inferences is superposed upon. We first apply our results to the equational case and to unfailing Knuth-Bendix completion. Second, we extend the techniques to the case of full first-order clauses with equality, proving the refutational completeness of a new simple inference system. Finally, it is briefly outlined how this method can be applied to further restrict inference systems by the use of ordering constraints.
dc.format.extent19 p.
dc.rightsAttribution-NonCommercial-NoDerivs 3.0 Spain
dc.subjectÀrees temàtiques de la UPC::Informàtica
dc.subject.lcshLogic, Symbolic and mathematical
dc.subject.lcshLogic programming
dc.titleBasic superposition is complete
dc.typeExternal research report
dc.subject.lemacLògica matemàtica
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