U. Hustadt and B.Konev (2003): TRP++ 2.0: A Temporal Resolution Prover

U. Hustadt and B.Konev (2003): ``TRP++ 2.0: A Temporal Resolution Prover.'' In F. Baader, editor, Proceedings of the 19th International Conference on Automated Deduction (CADE-19) [Miamia Beach, USA, July/August 2003], pp. 274-278. LNAI 2741, Springer.
Abstract, BiBTeX, PDF (© Springer), Abstract + PDF (Springer).

In this paper we present TRP++ Version 2.0, a theorem prover for propositional linear time logic PLTL. TRP++ is based on the resolution method for PLTL developed by Fisher which involves the translation of PLTL-formulae to separated normal form and the application of the inference rules of the temporal resolution calculus.