TRP++ is an experimental C++ implementation of a theorem prover for Propositional Linear Time Temporal Logic based on the temporal resolution calculus. It is released under the terms and conditions of the GNU General Public License v2 (or later).
The TRP++ source code Version 2.2. can be downloaded here. 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 (or compressed binary). Special thanks to Viktor Schuppan for a bugfix.
TRP++ accepts input in Separated Normal Form, the syntax is described in the input syntax document — 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.