Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Planning as Deductive Synthesis in Intuitionistic Linear Logic
Authors: Lucas Dixon ; Alan Smaill ; Alan Bundy
Date: 2006
Publication Type:Other Publication Status:Other
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
author = { Lucas Dixon and Alan Smaill and Alan Bundy },
title = {Planning as Deductive Synthesis in Intuitionistic Linear Logic},
year = 2006,
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh