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.
- Corrected an error in the initalisation of the loop search procedure tryTR, which could result in incorrect loops to be found.
- Corrected an error in additionalClausesBFS, which could result in the procedure failing unintentionally.
- Ported temporalResolution.pl to SWI-Prolog Version 5.6.x.
- Version 1.0 allows to resolve with initial clauses during loop search which can lead to incorrect results.
- Initial release
- C1ran (n = 5, k = 3, p = 0.5)
- C1ran (n = 12, k = 3, p = 0.5)
- C2ran (n = 5, k = 3, p = 0.5)
- C2ran (n = 12, k = 3, p = 0.5)