Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Tactic-based theorem proving in first-order modal and temporal logics
Authors: Claudio Castellini ; Alan Smaill
Date:Jun 2001
Publication Title:Proceedings of IJCAR 2001
Publication Type:Conference Paper
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.
2002 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
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},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh