Proof Planning for First-Order Temporal Logic

11 years 21 hour ago
Proof Planning for First-Order Temporal Logic
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...
Claudio Castellini, Alan Smaill
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where CADE
Authors Claudio Castellini, Alan Smaill
Comments (0)