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

  TRS: A Resolution-based Theorem Prover for Temporal Logic PLTL

   BCN Prototype: An implementation of Constructive Negation

   CS Prototype: An equality constraint solver