Tactic-based theorem proving in first-order modal and temporal logics

We describe the ongoing work on a tactic-based theorem prover for First-Order Modal and Temporal Logics (FOTLs for the temporal ones). In formal methods, especially temporal logics play a determining role; in particular, FOTLs are natural whenever the modeled systems are infinite-state. But reasoning in FOTLs is hard and few approaches have so far proved effective. Here we introduce a family of sequent calculi for first-order modal and temporal logics which is modular in the structure of time; moreover, we present a tactic-based modal/temporal theorem prover enforcing this approach, obtained employing the higher-order logic programming language lambda-Prolog. Finally, we show some promising experimental results and raise some open issues. We believe that, together with the Proof Planning approach, our system will eventually be able to improve the state of the art of formal methods through the use of FOTLs.