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.

Downloads for Windows and Linux (both include a collection of examples for easily first testing)

       Windows:    TTMv0-Setup.exe

            Linux:         ttm-prover.tar.gz  (md5sum = 01722bf87dc99e6fbee4dd11f2275142)


                32 bits: ttm-prover_0.8-1_i386.deb

                64 bits: ttm-prover_0.8-1_amd64.deb

                pub = 4096R/3B72450C 2011-12-28

                uid = Iker Salmón San Millán (shaola) <ikerssm at>

Comments are welcome to paqui.lucio at

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: January 31, 2014