Fundamental Results on Automated Theorem Proving by Test Set Induction

Adel Bouhoula 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We present in this paper a general scheme for test set induction procedure and describe a simple technique to prove the correctness of this procedure. Previously, we could only compute a test set for a conditional specification if the constructors were free. Here, we give a new definition of test sets and a procedure to compute them even if the constructors are not free. The method uses a new notion of provable inconsistency and induction prositions (that need to be instantiated by induction schemes) which allows us to refute more false conjectures than with previous approaches. We also present an algorithm to compute all the induction positions of a conditional specification. Finally, we propose an induction procedure which is refutationally complete for conditional specifications (not restricted to boolean specifications) in that it refutes any conjecture which is not an inductive theorem. The method has been implemented in SPIKE. Based on computer experiments, SPIKE appears to be more practical and efficient than related systems.
Type de document :
Rapport
[Research Report] RR-2478, INRIA. 1995, pp.50
Liste complète des métadonnées

https://hal.inria.fr/inria-00074196
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 14:43:53
Dernière modification le : jeudi 11 janvier 2018 - 06:19:58
Document(s) archivé(s) le : mardi 12 avril 2011 - 16:00:24

Fichiers

Identifiants

  • HAL Id : inria-00074196, version 1

Collections

Citation

Adel Bouhoula. Fundamental Results on Automated Theorem Proving by Test Set Induction. [Research Report] RR-2478, INRIA. 1995, pp.50. 〈inria-00074196〉

Partager

Métriques

Consultations de la notice

119

Téléchargements de fichiers

55