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:

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