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

Abstract : 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.
Type de document :
Communication dans un congrès
Proceedings of the International Conference on Automated Deduction, 1997, Townsville, Australia. Springer, 1249, pp.34-48, 1997, Lecture Notes on Computer Science
Liste complète des métadonnées

Littérature citée [28 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00536822
Contributeur : Joachim Niehren <>
Soumis le : mardi 16 novembre 2010 - 23:11:40
Dernière modification le : mardi 31 octobre 2017 - 14:22:18
Document(s) archivé(s) le : jeudi 17 février 2011 - 03:17:01

Fichiers

fullContext.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00536822, version 1

Citation

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. Springer, 1249, pp.34-48, 1997, Lecture Notes on Computer Science. 〈inria-00536822〉

Partager

Métriques

Consultations de la notice

51

Téléchargements de fichiers

51