Automatic Verification of Sufficient Completeness for Conditional Constrained Term Rewriting Systems - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2006

Automatic Verification of Sufficient Completeness for Conditional Constrained Term Rewriting Systems

Adel Bouhoula
  • Fonction : Auteur
  • PersonId : 756484
  • IdRef : 132449021
Florent Jacquemard

Résumé

We present a procedure for checking sufficient completeness for conditional and constrained term rewriting systems with 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 method 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 procedure is sound and complete. It has been successfully applied, 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.
Fichier principal
Vignette du fichier
RR-5863.pdf (353.5 Ko) Télécharger le fichier

Dates et versions

inria-00070163 , version 1 (19-05-2006)

Identifiants

  • HAL Id : inria-00070163 , version 1

Citer

Adel Bouhoula, Florent Jacquemard. Automatic Verification of Sufficient Completeness for Conditional Constrained Term Rewriting Systems. [Research Report] RR-5863, INRIA. 2006, pp.17. ⟨inria-00070163⟩
67 Consultations
102 Téléchargements

Partager

Gmail Facebook X LinkedIn More