The main goals of the project are:
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.