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.
Linux: ttm-prover.tar.gz (md5sum = 01722bf87dc99e6fbee4dd11f2275142)
Debian/Ubuntu:
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 gmail.com>
Comments are welcome to paqui.lucio at ehu.es
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