HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Automatic Verification of Sufficient Completeness for Conditional Constrained Term Rewriting Systems

Adel Bouhoula 1 Florent Jacquemard 1
1 SECSI - Security of information systems
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 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.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 7:18:04 PM
Last modification on : Friday, February 4, 2022 - 3:18:24 AM
Long-term archiving on: : Sunday, April 4, 2010 - 8:22:02 PM


  • HAL Id : inria-00070163, version 1


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⟩



Record views


Files downloads