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.