Sébastien Limet ; Pierre Réty - E-unification by means of tree tuple synchronized grammars

dmtcs:240 - Discrete Mathematics & Theoretical Computer Science, January 1, 1997, Vol. 1 - https://doi.org/10.46298/dmtcs.240
E-unification by means of tree tuple synchronized grammarsArticle

Authors: Sébastien Limet 1; Pierre Réty 1

  • 1 Laboratoire d'Informatique Fondamentale d'Orléans

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.


Volume: Vol. 1
Published on: January 1, 1997
Imported on: March 26, 2015
Keywords: E-unification,narrowing,tree languages,decidability,[INFO.INFO-DM] Computer Science [cs]/Discrete Mathematics [cs.DM]

8 Documents citing this article

Consultation statistics

This page has been seen 361 times.
This article's PDF has been downloaded 303 times.