A modular, tactic-based approach to first-order temporal theorem proving

In system specification and formal verification it is a central issue to deal with temporal logics. In particular, First- Order Temporal Logics (FOTLs) are needed whenever the modelled systems are infinite-state. Reasoning in FOTLs is hard and few approaches have so far proved effective. In this paper we propose a novel approach to FOTLs, in the style of labelled deduction in Quantified Modal Logics, which is modular in the structure of time and can therefore be adapted to a wide class of FOTLs. Moreover, we present a tactic-based temporal theorem prover enforcing this approach, obtained by applying Amy Felty’s work on higher-order theorem proving in lambda-Prolog. Finally, we show some promising experimental results.