Tenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1995)

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

Authors: H. Comon R. Nieuwenhuis A. Rubio


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.


    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}