Deductive synthesis of recursive plans in linear logic

Stephen Cresswell, Alan Smaill, Julian Richardson

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

Abstract

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
PublisherSpringer-Verlag
Pages252-264
Number of pages13
ISBN (Electronic)978-3-540-44657-6
ISBN (Print)978-3-540-67866-3
DOIs
Publication statusPublished - 1999

Publication series

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

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

Cite this