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.date.accessioned2020-10-14T10:18:27Z
dc.date.available2020-10-14T10:18:27Z
dc.date.issued1991-10-15
dc.identifier.citationNieuwenhuis, R.; Rubio, A. Basic superposition is complete. 1991.
dc.identifier.urihttp://hdl.handle.net/2117/330207
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.language.isoeng
dc.relation.ispartofseriesLSI-91-42
dc.rightsAttribution-NonCommercial-NoDerivs 3.0 Spain
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/3.0/es/
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
local.identifier.drac29559478
dc.description.versionPostprint (published version)
local.citation.authorNieuwenhuis, R.; Rubio, A.


Files in this item

Thumbnail

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