Fundamental Results on Automated Theorem Proving by Test Set Induction

Adel Bouhoula (1)

1 PROTHEO - Constraints, automatic deduction and software properties proofs

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.

Mots clés: automated reasoning; theorem proving; test set induction; simultaneous induction; term rewriting systems

Domaines: Autre [cs.OH]

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