Automated Theorem Proving by Test Set Induction

Test set induction is a goal-directed proof technique which combines the full power of explicit induction and proof by consistency. It works by computing an appropriate explicit induction scheme calleda test set, to trigger the induction proof, and then applies a refutation principle using proof by consistency techniques. We present a general scheme for test set induction together with a simple soundness proof. Our method is based on new notions of test sets,induction variables, andprovable inconsistency, which allow us to refute false conjectures even in the case where the functions are not completely defined. We show how test sets can be computed when the constructors are not free, and give an algorithm for computing induction variables. Finally, we present a procedure for proof by test set induction which is refutationally complete for a larger class of specifications than has been shown in previous work. The method has been implemented in the proverSPIKE. Based on computer experiments dealing with mutual induction,SPIKEappears to be more practical and efficient than explicit induction based systems.