Automating Sufficient Completeness Check for Conditional and Constrained TRS

Adel Bouhoula 1 Florent Jacquemard 2
2 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : We present a procedure for checking sufficient completeness for conditional and constrained term rewriting systems containing axioms for constructors which may be constrained (by e.g. equalities, disequalities, ordering, membership...). Such axioms allow to specify complex data structures like e.g. sets, sorted lists or powerlists. Our approach is integrated in a framework for inductive theorem proving based on tree grammars with constraints, a formalism which permits an exact representation of languages of ground constructor terms in normal form. The key technique used in the procedure is a generalized form of narrowing where, given a term, instead of unifying it with left members of rewrite rules, we instantiate it, at selected variables, following the productions of a constrained tree grammar, and test whether it can be rewritten. Our procedure is sound and complete and has been successfully applied to several examples, yielding very natural proofs and, in case of negative answer, a counter example suggesting how to complete the specification. Moreover, it is a decision procedure when the TRS is unconditional but constrained, for a large class of constrained constructor axioms.
Type de document :
Communication dans un congrès
Levy, Jordi. 20th International Workshop on Unification (UNIF), Aug 2006, Seattle, United States. 2006, Proceedings of the 20th International Workshop on Unification (UNIF)
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00579017
Contributeur : Florent Jacquemard <>
Soumis le : mardi 22 mars 2011 - 23:30:55
Dernière modification le : jeudi 11 janvier 2018 - 01:49:35
Document(s) archivé(s) le : jeudi 23 juin 2011 - 03:00:30

Fichier

BJ-unif06.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00579017, version 1

Collections

Citation

Adel Bouhoula, Florent Jacquemard. Automating Sufficient Completeness Check for Conditional and Constrained TRS. Levy, Jordi. 20th International Workshop on Unification (UNIF), Aug 2006, Seattle, United States. 2006, Proceedings of the 20th International Workshop on Unification (UNIF). 〈inria-00579017〉

Partager

Métriques

Consultations de la notice

155

Téléchargements de fichiers

96