Temporal logics are extensions of classical logic with operators that deal with time. They have been used in a wide variety of areas within Computer Science and Artificial Intelligence, for example robotics, databases, hardware verification and agent-based systems.
In particular, propositional temporal logics have been applied to (i) the specification and verification of reactive (e.g. distributed or concurrent) systems; (ii) the synthesis of programs from temporal specifications;; (iii) the semantics of executable temporal logic; (iv) algorithmic verification via model-checking; and (v) knowledge representation and reasoning.
In developing these techniques, temporal proof is often required, and we base our work on practical proof techniques for the clausal resolution method for propositional linear-time temporal logic PLTL. The method is based on an intuitive clausal form, called SNF, comprising three main clause types and a small number of resolution rules.
While the approach has been shown to be competitive using a prototype implementation of the method, we now aim at an even more efficient implementation. This implementation, called TRP++, is the focus of this paper[an error occurred while processing this directive]