5th International Conference on Rewriting Techniques and Applications, pp. 106-120, Springer-Verlag, June 1993
We present a new constraint system with equational and membership constraints over infinite trees. It provides for complete and
correct satisfiability and entailment tests and is therefore suitable
for the use in concurrent constraint programming systems
which are based on cyclic data structures.
of regular systems of equations with a deterministic form of union.
As the main technical particularity of the algorithms we present
a novel memorization technique.
We believe that both satisfiability and entailment tests can be
implemented in an efficient and incremental manner.
@INPROCEEDINGS{NPT:InfiniteMembersh,
title = {Equational and Membership Constraints for Infinite Trees},
author = {Joachim Niehren and Andreas Podelski and Ralf Treinen},
year = {1993},
month = {jun},
editor = {{Kirchner, Claude}},
publisher = {"Springer-Verlag"},
booktitle = {5th International Conference on Rewriting Techniques and Applications},
series = {{Lecture Notes in Computer Science, vol. 690}},
pages = {{106-120}},
address = {{Montreal, Canada}},
note = {"Extended version: DFKI Research Report RR-93-14"},
}