TRP (Temporal Resolution Prover)

TRP is a a protoypical implementation in Prolog of a theorem prover for propositional linear-time logic based on the temporal resolution calculus. It is also able to deal with certain combinations of linear-time logic with extensions of the basic modal logic K with one or more of the axiom schemata D, T, 4 and 5.

Strength and weaknesses of TRP have been analysed in Hustadt and Schmidt (2001) and Hustadt and Schmidt (2002b). In particular, the later paper contains a comparison with other decision procedures for propositional linear-time logic.

As a pure linear-time logic prover, TRP has been superseded by a C++ implementation of the same calculus, called TRP++, which can be found here.

Below you find the source code for TRP 1.4 which includes instructions on how to use it.

Changes:
1.4
Corrected an error in the initalisation of the loop search procedure tryTR, which could result in incorrect loops to be found.
1.3
Corrected an error in additionalClausesBFS, which could result in the procedure failing unintentionally.
1.2
Ported temporalResolution.pl to SWI-Prolog Version 5.6.x.
1.1
Version 1.0 allows to resolve with initial clauses during loop search which can lead to incorrect results.
1.0
Initial release
The samples we have used to compare TRP to other decision procedures for propositional linear-time logic are also available: The random generator itself is given by Prolog files: genpltl.pl and simplify.pl. Unfortunately, the files are not well-documented, but if you would like to use the generator, feel free to contact us.