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.

References in zbMATH (referenced in 18 articles )

Showing results 1 to 18 of 18.
Sorted by year (citations)

  1. Griggio, Alberto; Roveri, Marco; Tonetta, Stefano: Certifying proofs for SAT-based model checking (2021)
  2. Hustadt, Ullrich; Ozaki, Ana; Dixon, Clare: Theorem proving for pointwise metric temporal logic over the naturals via translations (2020)
  3. Li, Jianwen; Zhu, Shufang; Pu, Geguang; Zhang, Lijun; Vardi, Moshe Y.: SAT-based explicit LTL reasoning and its application to satisfiability checking (2019)
  4. Reynolds, Mark: A new rule for LTL tableaux (2016)
  5. Schuppan, Viktor: Extracting unsatisfiable cores for LTL via temporal resolution (2016)
  6. Schuppan, Viktor: Enhancing unsatisfiable cores for LTL with information on temporal relevance (2016)
  7. Hustadt, Ullrich; Gainer, Paul; Dixon, Clare; Nalon, Cláudia; Zhang, Lan: Ordered resolution for coalition logic (2015)
  8. Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare: A modal-layered resolution calculus for K (2015)
  9. Suda, Martin: Variable and clause elimination for LTL satisfiability checking (2015)
  10. Gaintzarain, Jose; Hermo, Montserrat; Lucio, Paqui; Navarro, Marisa; Orejas, Fernando: Invariant-free clausal temporal resolution (2013)
  11. Schmidt, Renate A.; Hustadt, Ullrich: First-order resolution methods for modal logics (2013)
  12. Kamide, Norihiro: Bounded linear-time temporal logic: a proof-theoretic investigation (2012)
  13. Schuppan, Viktor: Towards a notion of unsatisfiable and unrealizable cores for LTL (2012)
  14. Zhang, Lan; Hustadt, Ullrich; Dixon, Clare: CTL-RP: A computation tree logic resolution prover (2010)
  15. Zhang, Lan; Hustadt, Ullrich; Dixon, Clare: A refined resolution calculus for CTL (2009)
  16. Dixon, Clare: Using temporal logics of knowledge for specification and verification -- a case study (2006)
  17. Kutz, Oliver; Lutz, Carsten; Wolter, Frank; Zakharyaschev, Michael: (\mathcalE)-connections of abstract description systems (2004)
  18. Hustadt, Ullrich; Konev, Boris: TRP++ 2.0: a temporal resolution prover. (2003) ioport