Unification and Matching in Hierarchical Combinations of Syntactic Theories

Serdar Erbatur 1 Deepak Kapur 2 Andrew Marshall 3 Paliath Narendran 4 Christophe Ringeissen 5
1 Ludwig-Maximilians-Universität München
2 The University of New Mexico [Albuquerque]
3 University of Mary Washington
4 University at Albany
5 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : We investigate a hierarchical combination approach to the unification problem in non-disjoint unions of equational theories. In this approach, the idea is to extend a base theory with some additional axioms given by rewrite rules in such way that the unification algorithm known for the base theory can be reused without loss of completeness. Additional techniques are required to solve a combined problem by reducing it to a problem in the base theory. In this paper we show that the hierarchical combination approach applies successfully to some classes of syntactic theories, such as shallow theories since the required unification algorithms needed for the combination algorithm can always be obtained. We also consider the matching problem in syntactic extensions of a base theory. Due to the more restricted nature of the matching problem, we obtain several improvements over the unification problem.
Type de document :
Communication dans un congrès
Carsten Lutz and Silvio Ranise. Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Sep 2015, Wroclaw, Poland. Springer, 9322, pp.291--306, Lecture Notes in Computer Science. 〈10.1007/978-3-319-24246-0_18〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-01206669
Contributeur : Christophe Ringeissen <>
Soumis le : mardi 29 septembre 2015 - 14:34:24
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : mercredi 30 décembre 2015 - 10:42:12

Fichier

combi-syntactic.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | UNIV-FCOMTE | UNIV-BM | FEMTO-ST | UNIV-BM-THESE | UNIV-LORRAINE | LORIA-FM | LORIA

Citation

Serdar Erbatur, Deepak Kapur, Andrew Marshall, Paliath Narendran, Christophe Ringeissen. Unification and Matching in Hierarchical Combinations of Syntactic Theories. Carsten Lutz and Silvio Ranise. Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Sep 2015, Wroclaw, Poland. Springer, 9322, pp.291--306, Lecture Notes in Computer Science. 〈10.1007/978-3-319-24246-0_18〉. 〈hal-01206669〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

274

Téléchargements de fichiers

94

Contact


archive-ouverte@inria.fr