SPIKE: A system for sufficient completeness and parameterized inductive proofs

Abstract

The system SPIKE is an automated system for theorem proving in theories presented by a set of Horn clauses with equality. SPIKE is written in Caml Light and contains more than 10000 lines of code. It runs on SUN4 workstations under Unix with a graphical user-friendly interface in Xwindow system realized in Tk. It has been designed to provide users with facilities to direct and monitor proofs easily. The main novelty is the use of a new inference rule, which permit us to prove and disprove automatically inductive properties in parameterized conditional specifications [Bou93]. The motivation for this is that theorem proving in parameterized specifications allows for shorter and more structured proofs. Moreover, a generic proof can be given only once and reused for each instantiation of the parameters. Our procedure also extends our previous work [BR93a] to non-free constructors. Based on computer experiments, the method appears to be more practical and efficient than inductive proofs in non-parameterized specifications. We have also implemented a new procedure for testing sufficient completeness for parameterized conditional specifications [Bou93]. Moreover, SPIKE offers facilities to check and complete definitions.