TRP++ : Temporal Resolution Prover

The main goals of the project are:

• Developing a robust, and relatively efficient version of the clausal resolution approach to propositional temporal logic;
• Creating an experimental environment to try different modifications of temporal resolution;
• Demonstrating that a temporal resolution-based prover is competitive with other known proof search techniques.

The current version of the statically linked TRP++ Linux binary can be downloaded from here TRP++ Version 2.0 (about 1.2Mb). Alternatively, download the compressed binary of TRP++ Version 2.0 (about 480 Kb).

TRP++ accepts input in Separated Normal Form, the syntax is described in input syntax; it is the same as the input of another temporal resolution-based prover, TRP by Ullrich Hustadt (in fact, TRP++ shares many implementation ideas with TRP).

A paper describing TRP++ version 1.0 was presented at the 3d International Workshop on the Implementation of Logics; the paper is available on the workshop site, or locally.

Some examples of input can be found here.

Example of usage: trp++ test4.in

New: A translator from the PTL syntax to the TRP++ format is available. It is written in OCaml. This is my first and only program in OCaml, please report any errors.