Automated Induction with Constrained Tree Automata

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 propose a procedure for automated implicit inductive theorem proving for equational specifications made of rewrite rules with conditions and constraints. The constraints are interpreted over constructor terms (representing data values), and may express syntactic equality, disequality, ordering and also membership in a fixed tree language. Constrained equational axioms between constructor terms are supported and can be used in order to specify complex data structures like sets, sorted lists, trees, powerlists... Our procedure is based on tree grammars with constraints, a formalism which can describe exactly the initial model of the given specification (when it is sufficiently complete and terminating). They are used in the inductive proofs first as an induction scheme for the generation of subgoals at induction steps, second for checking validity and redundancy criteria by reduction to an emptiness problem, and third for defining and solving membership constraints. We show that the procedure is sound and refutationally complete. It generalizes former test set induction techniques and yields natural proofs for several non-trivial examples presented in the paper, these examples are difficult (if not impossible) to specify and carry on automatically with other induction procedures.
Type de document :
Communication dans un congrès
Alessandro Armando and Peter Baumgartner and Gilles Dowek. 4th International Joint Conference on Automated Reasoning (IJCAR), Aug 2008, Sydney, Australia. Springer, 5195, pp.539-554, 2008, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/2t58870130542x16/〉. 〈10.1007/978-3-540-71070-7_44〉
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00579004
Contributeur : Florent Jacquemard <>
Soumis le : mardi 22 mars 2011 - 21:04:24
Dernière modification le : mardi 5 juin 2018 - 15:54:02
Document(s) archivé(s) le : jeudi 23 juin 2011 - 02:58:14

Fichier

induction-HAL.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Adel Bouhoula, Florent Jacquemard. Automated Induction with Constrained Tree Automata. Alessandro Armando and Peter Baumgartner and Gilles Dowek. 4th International Joint Conference on Automated Reasoning (IJCAR), Aug 2008, Sydney, Australia. Springer, 5195, pp.539-554, 2008, Lecture Notes in Computer Science. 〈http://www.springerlink.com/content/2t58870130542x16/〉. 〈10.1007/978-3-540-71070-7_44〉. 〈inria-00579004〉

Partager

Métriques

Consultations de la notice

217

Téléchargements de fichiers

139