Sufficient Completeness Verification for Conditional and Constrained Term Rewriting Systems

Adel Bouhoula 1 Florent Jacquemard 2
2 MuTant - Synchronous Realtime Processing and Programming of Music Signals
Inria Paris-Rocquencourt, UPMC - Université Pierre et Marie Curie - Paris 6, IRCAM, CNRS - Centre National de la Recherche Scientifique
Abstract : We present a procedure for checking sufficient completeness of 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 into 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 procedure is presented by an inference system which is shown sound and complete. A precondition of one inference of this system refers to a (undecidable) property called strong ground reducibility which is discharged to the above inductive theorem proving system. We have successfully applied our method to several examples, yielding readable proofs and, in case of negative answer, a counter-example suggesting how to complete the specification. Moreover, we show that it is a decision procedure when the TRS is unconditional but constrained, for an expressive class of constrained constructor axioms.
Type de document :
Article dans une revue
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00643136
Contributeur : Florent Jacquemard <>
Soumis le : lundi 21 novembre 2011 - 11:49:45
Dernière modification le : mercredi 12 décembre 2018 - 01:35:20
Document(s) archivé(s) le : mercredi 22 février 2012 - 02:25:26

Fichier

completeness-long.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Adel Bouhoula, Florent Jacquemard. Sufficient Completeness Verification for Conditional and Constrained Term Rewriting Systems. Journal of Applied Logic, Elsevier, 2012, 10 (1), pp.127-143. 〈http://www.sciencedirect.com/science/article/pii/S1570868311000413〉. 〈10.1016/j.jal.2011.09.001〉. 〈hal-00643136〉

Partager

Métriques

Consultations de la notice

295

Téléchargements de fichiers

215