The goat of this paper is both to give a E-unification procedure that always terminates, and to decide unifiability. For this, we assume that the equational theory is specified by a confluent and constructor-based rewrite system, and that four additional restrictions are satisfied. We give a procedure that represents the (possibly infinite) set of solutions thanks to a new kind of grammar, called tree tuple synchronized grammar, and that can decide unifiability thanks to an emptiness test. Moreover we show that if only three of the four additional restrictions are satisfied then unifiability is undecidable.
CITATION STYLE
Limet, S., & Réty, P. (1997). E-unification by means of tree tuple synchronized grammars. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1214, pp. 429–440). Springer Verlag. https://doi.org/10.1007/bfb0030616
Mendeley helps you to discover research relevant for your work.