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 TRP++ source code can be downloaded from here TRP++Version 2.2. It compiles under Linux and Mac provided you have the necessary GNU development tools. Alternatively, you can try the current version of the statically linked TRP++ Linux binary, which can be downloaded from here TRP++ Version 2.2 (or the compressed binary of TRP++ Version 2.2). Special thanks to Viktor Schuppan for a bugfix.

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

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.