Proof planning for first-order temporal logic

Claudio Castellini, Alan Smaill

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationAutomated Deduction--CADE-20
Subtitle of host publication20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005. Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages15
ISBN (Electronic)978-3-540-31864-4
ISBN (Print)978-3-540-28005-7
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'Proof planning for first-order temporal logic'. Together they form a unique fingerprint.

Cite this