Implementation

The method described above has been implemented as a part of a prototype prover for temporal specifications in the $\lambda Clam$ envinronment [RSG98]. $\lambda Clam$ is a proof planning [Bun88] system, implemented in the Teyjus implementation of $\lambda$Prolog [Tey,Lpro], a higher-order typed logic programming language A proof plan is a representation of a proof at some level of abstraction (usually above the level of basic inference rules, but not necessarily so). In $\lambda Clam$ a proof plan is generated from a goal by the application of planning operators called proof methods. Atomic methods are suitable for the implementation of basic proof rules, or automated proof procedures, while compound methods are used to build more complex proof strategies (or heuristics) from atomic methods. The features of the system are as follows:

• Our system works with arithmetical translations of temporal formulae, i.e. with translation into two-sorted first-order formulae, with one sort being the natural numbers. This is done for better integration with a body of proof plans and methods already existing in $\lambda Clam$ for arithmetic.
• For first-order (non-temporal) proving called within the prover an atomic method proof_tableau re-implementing the simple, but convenient LeanTap tableaux prover [BP95] in $\lambda$Prolog, is used. Higher-order unification and $\lambda$-terms as the data structure in $\lambda Prolog$ allows us to re-implement LeanTap in more direct and declarative way, without using the "non-logical" copy_term predicate and with $\lambda$-terms presenting the quantifier's bindings. Efficiency of such $\lambda$LeanTap proves to be comparable with the original LeanTap, running on Sicstus Prolog [Lis03].
• We have inplemented, so far, the simplest strategy concerning the depth of search within first-order tableau prover - it is invoked with the pre-defined constant depth bound. We consider the possibility to use the proof planning methodology to control the depth of search. Simple heuristics based on the number of quantifiers (or quantifier depth) may be used here.
• The kernel of the system is an atomic method called mutual_induction, implementing the above procedure. It uses the higher-order unification of $\lambda Prolog$ to separate a given a set of formulae into the sets of step rules and the universal and start parts, and also to produce subformulae, which are used later to construct the goals for first-order theorem proving (conditions to check in the Stages 1-4.) After that, mutual_induction invokes four sub-methods ($\lambda$-Prolog predicates) implementing the Stages 1-4 of the procedure.
• The sets of formulae are presented as Prolog lists and a simple procedure for generating all its subsets is used. Simple optimization, based on the fact that any superset of an inconsistent set of formulae is itself inconsistent, is applied at Stage 1. It remains to be explored whether the use of higher-order features of $\lambda Prolog$ may optimize the search for minimal inconsistent subsets.

Initial experiments have indicated the viability of our approach. The system is able to prove all the examples of temporal specifications given in [BDFL02]. Our further work is to develop and implement optimizations for the proof search procedure together with imporved strategies/heuristics.