Tech Reports

ULCS-04-004

TeMP: A Temporal Monodic Prover

Ullrich Hustadt, Boris Konev, Alexandre Riazanov and Andrei Voronkov


Abstract

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]