Lics

ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Tenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1995)

Paper: Orderings, AC-theories and Symbolic Constraint Solving (at LICS 1995)

Authors: Hubert Comon-Lundh Robert Nieuwenhuis Albert Rubio

Abstract

We design combination techniques for symbolic constraint solving in the presence of associative and commutative (AC) function symbols. This yields an algorithm for solving AC-RPO constraints where AC-RPO is the AC-compatible total reduction ordering of Nieuwenhuis and Rubio (Proc. RTA 93). This was a missing ingredient for automated deduction strategies with AC-constraint inheritance. As in the AC-unification case (actually the AC- unification algorithm is an instance of ours), we first study the pure case, i.e. we show how to solve AC-ordering constraints built over a single AC function symbol and variables. Since AC-RPO is an interpretation-based ordering, our algorithm also requires the combination of algorithms for solving interpreted constraints and non-interpreted constraints.

BibTeX

  @InProceedings{ComonLundhNieuwenhu-OrderingsACtheories,
    author = 	 {Hubert Comon-Lundh and Robert Nieuwenhuis and Albert Rubio},
    title = 	 {Orderings, AC-theories and Symbolic Constraint Solving},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)},
    year =	 {1995},
    month =	 {June}, 
    pages =      {375--385},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2022-10-3113:49
Sam Staton