Paper: Orderings, AC-theories and Symbolic Constraint Solving (at LICS 1995)
Authors: H. Comon R. Nieuwenhuis A. RubioAbstract
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} }