Theorem Proving in First-Order Temporal Logic

This page describes implementations initiated within the project Mechanising Firs-Order Temporal Logics, EPSRC grant GR/M466631.

MInd: Invariant Search via Temporal resolution

MInd(Mutual Induction) is an implementation of a method for a searching for invariants in the theorem proving for first-order temporal logic. The method is described in [1] and based on clausal temporal resolution technique [5]. It is implemented in the proof planning system $\lambda$ Clam [10] using the advantages of the higher-order logical programming language $\lambda$ Prolog. [9]. Its first version has been implemented by James Brotherston in March 2002. Since then it has been extended and modified by myself (A. Lisitsa).

More detailed descriptions can be found here:

• A. Lisitsa and J. Brotherston. Implementing invariant search via temporal resolution in Proceedings of 3rd Intenational workshop on the Implementation of Logics, Tbilisi, Georgia, Oct. 2002, pp. 15-19.

• Invariant Search via Temporal Resolution

$\lambda$ Clam module for MInd can be downloaded from here:

• MInd module and Signature (Version 0.3)

In order to be able use MInd one needs to install $\lambda$ Clam proof planning system, which in turn is implemented in Teyjus $\lambda$ Prolog. The following pages contain relevant resources.

• $\lambda$ Clam page
• $\lambda$ Prolog page
• Teyjus implementation of $\lambda$ Prolog

$\lambda$ LeanTap: lean deduction in $\lambda$Prolog

For first-order (non-temporal) proving called within the MInd system the simple, but convenient LeanTap tableaux prover [2] has been re-implemented in $\lambda$Prolog (Teyjus). Higher-order unification and $\lambda$-terms as the data structure in $\lambda$ Prolog allows 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.

More detailed description can be found here:

• A. Lisitsa. $\lambda$ LeanTap: lean deduction in $\lambda$ Prolog, University of Liverpool Department of Computer Science Technical Report ULCS-03-17, 2003 (to appear).

$\lambda$-LeanTap can be downloaded from here:

• $\lambda$ LeanTap