- Abstract:
-
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.
- Copyright:
- 2002 by The University of Edinburgh. All Rights Reserved
- Links To Paper
- No links available
- Bibtex format
- @InProceedings{EDI-INF-RR-0155,
- author = {
Claudio Castellini
and Alan Smaill
},
- title = {Tactic-based theorem proving in first-order modal and temporal logics},
- book title = {Proceedings of IJCAR 2001},
- year = 2001,
- month = {Jun},
- }
|
