Logic in Computer Science (LICS 2000)

Paper: Paramodulation with Built-In Abelian Groups (at LICS 2000)

Authors: Guillem Godoy Robert Nieuwenhuis

Abstract

A new technique is presented for superposition with first-order clauses with built-in abelian groups (AG). Compared with previous approaches, it is simpler, and no inferences with the AG axioms or abstraction rules are needed. Furthermore, AG-unification is used instead of the computationally more expensive unification modulo associativity and commutativity. Due to the simplicity and restrictiveness of our inference system, its compatibility with redundancy notions and constraints, and the fact that standard term orderings like RPO can be used, we believe that our technique will become the method of choice for practice, as well as a basis for new theoretical developments like logic-based complexity and decidability analysis.

BibTeX

  @InProceedings{GodoyNieuwenhuis-ParamodulationwithB,
    author = 	 {Guillem Godoy and Robert Nieuwenhuis},
    title = 	 {Paramodulation with Built-In Abelian Groups},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {413--424},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }