- Abstract:
- We describe a formalisation in Isabelle/HOL of Intuitionistic Linear Logic and consider the support this provides for constructing plans using deductive synthesis of the proof terms. Our representation is more expressive than traditional accounts of planning, provides an elegant solution to the frame problem, and supports attaching domain specific constraints to synthesis. Such constraints naturally support both contingent and conformant planning. Within this setting, different planning algorithms are implemented as search strategies within the proof assistant. This allows us to provide a flexible and soundness-preserving methodology for developing search strategies.
- Links To Paper
- Personal copy
- Bibtex format
- @Misc{EDI-INF-RR-0786,
- author = {
Lucas Dixon
and Alan Smaill
and Alan Bundy
},
- title = {Planning as Deductive Synthesis in Intuitionistic Linear Logic},
- year = 2006,
- url = {http://homepages.inf.ed.ac.uk/ldixon/papers/infrep-06-planill.pdf},
- }
|
