Verified Planning by Deductive Synthesis in Intuitionistic Linear Logic

L. Dixon, A. Smaill, Alan Bundy

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


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 flexible 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 significant symmetry in search, caused by context splitting, can be pruned by using a derived inference rule. Secondly, we show how domain specific constraints on synthesis are supported and how they can be used to find contingent or conformant plans. We illustrate the approach with example planning scenarios.
Original languageEnglish
Title of host publicationWorkshop on Verification and Validation of Planning and Scheduling Systems: ICALP 2009
Number of pages10
Publication statusPublished - 2009


Dive into the research topics of 'Verified Planning by Deductive Synthesis in Intuitionistic Linear Logic'. Together they form a unique fingerprint.

Cite this