swMATH ID: 14679
Software Authors: Hustadt, U., Konev, B.
Description: 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.
Homepage: https://cgi.csc.liv.ac.uk/~konev/software/trp++/
Related Software: NuSMV; MiniSat; TSPASS; SPASS; nuXmv; TeMP; TTM; BGL; Boost; Boost C++ Libraries; E Theorem Prover; CTL-RP; CAVA LTL Modelchecker; AIGER; MathSAT5; GitHub; InKreSAT; SPOT; SPIN; LOUI
Referenced in: 17 Publications

Referencing Publications by Year