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.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Schuppan, Viktor: Extracting unsatisfiable cores for LTL via temporal resolution (2016)
- Suda, Martin: Variable and clause elimination for LTL satisfiability checking (2015)
- Gaintzarain, Jose; Hermo, Montserrat; Lucio, Paqui; Navarro, Marisa; Orejas, Fernando: Invariant-free clausal temporal resolution (2013)
- Kamide, Norihiro: Bounded linear-time temporal logic: a proof-theoretic investigation (2012)
- Schuppan, Viktor: Towards a notion of unsatisfiable and unrealizable cores for LTL (2012)
- Dixon, Clare: Using temporal logics of knowledge for specification and verification -- a case study (2006)
- Kutz, Oliver; Lutz, Carsten; Wolter, Frank; Zakharyaschev, Michael: $\cal E$-connections of abstract description systems (2004)