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

Claudio Castellini, Alan Smaill

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationProceedings of International Conference on Temporal Logic (ICTL 2000)
Number of pages12
Publication statusPublished - 2000


Dive into the research topics of 'A modular, tactic-based approach to first-order temporal theorem proving'. Together they form a unique fingerprint.

Cite this