Paper: On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups (at LICS 2001)

Authors: Guillem Godoy Robert Nieuwenhuis

Abstract

It is crucial for the performance of ordered resolution or paramodulation-based deduction systems that they incorporate specialized techniques to work efficiently with standard algebraic theories E. Essential ingredients for this purpose are term orderings that are E-compatible, for the given E, and algorithms deciding constraint satisfiability for such orderings. Here we introduce a uniform technique providing the first such algorithms for some orderings for abelian semigroups, abelian monoids and abelian groups, which we believe will lead to reasonably efficient techniques for practice. The algorithms are optimal since we show that, for any well-founded E-compatible ordering for these E, the constraint satisfiability problem is NP-hard even for conjunctions of inequations, and our algorithms are in NP.

BibTeX

  @InProceedings{GodoyNieuwenhuis-OnOrderingConstrain,
    author = 	 {Guillem Godoy and Robert Nieuwenhuis},
    title = 	 {On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups},
    booktitle =  {Proceedings of the Sixteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2001)},
    year =	 {2001},
    month =	 {June}, 
    pages =      {38--47},
    location =   {Boston, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }