Paper: Paramodulation with Non-Monotonic Orderings (at LICS 1999)
Abstract
All current completeness results for ordered paramodulation require the term ordering \mathto be well-founded, monotonic and total(izable) on ground terms. Here we introduce a new proof technique where the only properties required for \mathare well-foundedness and the subterm property¹ The technique is a relatively simple and elegant application of some fundamental results on the termination and confluence of ground term rewrite systems (TRS). By a careful further analysis of our technique, we obtain the first Knuth-Bendix completion procedure that finds a convergent TRS for a given set of equations E and a (possibly non-totalizable) reduction ordering \mathwhenever it exists² Note that being a reduction ordering is the minimal possible requirement on \math, since a TRS terminates if, and only if, it is contained in a reduction ordering.
BibTeX
@InProceedings{BofillGodoyNieuwenh-ParamodulationwithN, author = {Miquel Bofill and Guillem Godoy and Robert Nieuwenhuis and Albert Rubio}, title = {Paramodulation with Non-Monotonic Orderings}, booktitle = {Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999)}, year = {1999}, month = {July}, pages = {225--233}, location = {Trento, Italy}, publisher = {IEEE Computer Society Press} }