- Abstract:
-
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.
- Copyright:
- 2002 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @InProceedings{EDI-INF-RR-0152,
- author = {
Claudio Castellini
and Alan Smaill
},
- title = {A modular, tactic-based approach to first-order temporal theorem proving},
- book title = {Proceedings of ICTL 2000},
- year = 2000,
- month = {Oct},
- }
|