Deductive synthesis of recursive plans in linear logic

Stephen Cresswell, Alan Smaill, Julian Richardson

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


Linear logic has previously been shown to be suitable for describing and deductively solving planning problems involving conjunction and disjunction. We introduce a recursively defined datatype and a corresponding induction rule, thereby allowing recursive plans to be synthesised. In order to make explicit the relationship between proofs and plans, we enhance the linear logic deduction rules to handle plans as a form of proof term.
Original languageEnglish
Title of host publicationRecent Advances in AI Planning
Subtitle of host publication5th European Conference on Planning, ECP’99, Durham, UK, September 8-10, 1999. Proceedings
Number of pages13
ISBN (Electronic)978-3-540-44657-6
ISBN (Print)978-3-540-67866-3
Publication statusPublished - 1999

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Dive into the research topics of 'Deductive synthesis of recursive plans in linear logic'. Together they form a unique fingerprint.

Cite this