TTM:  A Tableau-based Theorem Prover for Temporal Logic PLTL

TTM is a theorem prover for the Propositional Linear Temporal Logic called PLTL.

TTM allows you to test the satisfiability of any set of PLTL-formulas.

TTM is based on a one-pass tableau method for PLTL called the context-based tableau method.

TTM has been implemented in Haskell using the Glasgow Haskell Compiler.

Download

        Preliminary Version for Windows: TTMv0-Setup.exe

         This setup include a collection of examples for easily first testing

Please send comments, bugs and requests concerning to TTM to paqui.lucio@ehu.es

Related Publications

Dual Systems of Tableaux and Sequents for PLTL

J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F. Orejas
The Journal of Logic and Algebraic Programming 78: 701–722, (2009)

[JLAP09.pdf]  [BibTeX ] [Electronic Edition]

A Cut-Free and Invariant-Free Sequent Calculus for PLTL
J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro, and F.Orejas
In J. Duparc and T.A. Henzinger (Eds.): Computer Science Logic : 21 International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne,

Switzerland, September 11-15, 2007, LNCS 4646, pp. 481–495, Springer-Verlag Berlin Heidelberg, 2007.
[csl07.pdf] [BibTeX ] [Electronic Edition]

Systematic Semantic Tableaux for PLTL
J. Gaintzarain, M. Hermo, P. Lucio, M. Navarro

In VII Jornadas sobre Programación y Lenguajes, PROLE’2007, Zaragoza, Spain, September, 2007,

Revised Selected Paper in ENTCS 206, pp. 59-73, 2008

[prole07b.pdf] [BibTeX ] [Electronic Edition]

This work has been partially supported by the Spanish Project TIN2007-66523 and the Basque Project LoRea GIU07/35.

Last Modified: October 18th, 2011