Tech Reports


TeMP: A Temporal Monodic Prover

Ullrich Hustadt, Boris Konev, Alexandre Riazanov and Andrei Voronkov


We present TeMP - the first experimental system for testing validity of monodic temporal logic formulae. The prover implements fine-grained temporal resolution. The core operations required by the procedure are performed by an efficient resolution-based prover for classical first-order logic.

[Full Paper]