Informatics Report Series


Report   

EDI-INF-RR-0290


Related Pages

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

Home
Title:Proof Planning for First-Order Temporal Logic
Authors: Claudio Castellini ; Alan Smaill
Date:Jul 2005
Publication Title:Automated Deduction -- CADE2005
Publisher:Springer-Verlag
Publication Type:Conference Paper Publication Status:Published
Page Nos:235-249
ISBN/ISSN:3-540-2800
Abstract:
Proof planning is an automated reasoning technique which improves proof search by raising it to a meta-level. In this paper we apply proof planning to First-Order Linear Temporal Logic FOLTL, which can be seen as a quantified version of Linear Temporal Logic, overcoming its finitary limitation. Automated reasoning in FOLTL is hard, since it is non-recursively enumerable; but its expressiveness can be exploited to precisely model the behaviour of complex, infinite-state systems. In order to demonstrate the potentiality of our technique, we introduce a case-study inspired by the Feature Interactions problem and we model it in FOLTL; we then describe a set of methods which tackle and solve the validation problem for a number of properties of the model; and lastly we present a set of experimental results showing that the methods we propose capture the common patterns in the proofs presented, guide the search at the object level and let the overall system build large and highly structured proofs. This paper to some extent improves over previous work that showed how proof planning can be used to detect such interactions.
Copyright:
2005 by The University of Edinburgh. All Rights Reserved
Links To Paper
No links available
Bibtex format
@InProceedings{EDI-INF-RR-0290,
author = { Claudio Castellini and Alan Smaill },
title = {Proof Planning for First-Order Temporal Logic},
book title = {Automated Deduction -- CADE2005},
publisher = {Springer-Verlag},
year = 2005,
month = {Jul},
pages = {235-249},
}


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