TRP++ : Temporal Resolution Prover

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 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.


Logic and Computation Group at the Department of Computer Science
Konev@liverpool.ac.uk,