## 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.

- TRP (Version 1.4) for SWI-Prolog: This version requires SWI-Prolog Version 5.6.x to run.
- TRP (Version 1.4) for SICStus Prolog: This version requires SICStus Prolog Version 3.8.x to run.

- 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

*C*(n = 5, k = 3, p = 0.5)^{1}_{ran}*C*(n = 12, k = 3, p = 0.5)^{1}_{ran}*C*(n = 5, k = 3, p = 0.5)^{2}_{ran}*C*(n = 12, k = 3, p = 0.5)^{2}_{ran}