Logic in Computer Science (LICS 1995)

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

Authors: H. Comon R. Nieuwenhuis A. 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{ComonNieuwenhuisRub-OrderingsACtheories,
    author = 	 {H. Comon and R. Nieuwenhuis and A. Rubio},
    title = 	 {Orderings, AC-theories and Symbolic Constraint Solving},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {375-385},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }