Skip to Main content Skip to Navigation
Journal articles

E-unification by means of tree tuple synchronized grammars

Abstract : The goal of this paper is both to give an 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 tree tuple synchronized grammar, and that can decide upon unifiability thanks to an emptiness test. Moreover, we show that if only three of the four additional restrictions are satisfied then unifiability is undecidable.
Document type :
Journal articles
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download
Contributor : Alain Monteil Connect in order to contact the contributor
Submitted on : Wednesday, March 5, 2014 - 9:31:17 AM
Last modification on : Saturday, June 25, 2022 - 10:12:30 AM
Long-term archiving on: : Thursday, June 5, 2014 - 10:52:26 AM


Files produced by the author(s)




Sébastien Limet, Pierre Réty. E-unification by means of tree tuple synchronized grammars. Discrete Mathematics and Theoretical Computer Science, DMTCS, 1997, Vol. 1, pp.69-98. ⟨10.46298/dmtcs.240⟩. ⟨hal-00955691⟩



Record views


Files downloads