TRP++

TRP++: a 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.