Paper: Paramodulation with Non-Monotonic Orderings (at LICS 1999)

Authors: Miquel Bofill Guillem Godoy Robert Nieuwenhuis Albert Rubio

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}
  }