On Equality Up-to Constraints over Finite Trees, Context Unification and One-Step Rewriting - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 1997

On Equality Up-to Constraints over Finite Trees, Context Unification and One-Step Rewriting

Résumé

We introduce equality up-to constraints over finite trees and investigate their expressiveness. Equality up-to constraints subsume equality constraints, subtree constraints, and one-step rewriting constraints. We establish a close correspondence between equality up-to constraints over finite trees and context unification. Context unification subsumes string unification and is subsumed by linear second-order unification. We obtain the following three new results. The satisfiability problem of equality up-to constraints is equivalent to context unification, which is an open problem. The positive existential fragment of the theory of one-step rewriting is decidable. The E*A*E* fragment of the theory of context unification is undecidable.
Fichier principal
Vignette du fichier
fullContext.pdf (288.01 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00536822 , version 1 (16-11-2010)

Identifiants

  • HAL Id : inria-00536822 , version 1

Citer

Joachim Niehren, Manfred Pinkal, Peter Ruhrberg. On Equality Up-to Constraints over Finite Trees, Context Unification and One-Step Rewriting. Proceedings of the International Conference on Automated Deduction, 1997, Townsville, Australia. pp.34-48. ⟨inria-00536822⟩
51 Consultations
104 Téléchargements

Partager

Gmail Facebook X LinkedIn More