Informatics Report Series


Report   

EDI-INF-RR-0152


Related Pages

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

Home
Title:A modular, tactic-based approach to first-order temporal theorem proving
Authors: Claudio Castellini ; Alan Smaill
Date:Oct 2000
Publication Title:Proceedings of ICTL 2000
Publication Type:Conference Paper
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},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh