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


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 = 	 {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: 2017-04-0512:37
Andrzej Murawski