Veriﬁed Planning by Deductive Synthesis in Intuitionistic Linear Logic
Workshop on Verification and Validation of Planning and Scheduling Systems: ICALP 2009
MetadataShow full item record
We describe a new formalisation in Isabelle/HOL of Intuitionistic Linear Logic and consider the support this provides for constructing plans by proving the achievability of given planning goals. The plans so found are provably correct, by construction. This representation of plans in linear logic provides a concise account of planning with sensing actions, allows the creation and deletion of objects, and solves the frame problem in an elegant way. Within this setting, we show how planning algorithms are implemented as search strategies within a theorem proving system. This allows us to provide a ﬂexible methodology for developing search strategies that is independent of soundness issues. This feature is illustrated in two ways. Firstly, following ideas from logic programming, we show how a signiﬁcant symmetry in search, caused by context splitting, can be pruned by using a derived inference rule. Secondly, we show how domain speciﬁc constraints on synthesis are supported and how they can be used to ﬁnd contingent or conformant plans. We illustrate the approach with example planning scenarios.