Deductive synthesis of recursive plans in linear logic

Stephen Cresswell, Alan Smaill, Julian Richardson

Research output: Contribution to conferencePaper

21 Downloads (Pure)

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
Pages252-264
Number of pages13
Publication statusPublished - 8 Sep 1999
Event5th European Conference on Planning (ECP 99) - Durham, England
Duration: 8 Sep 199910 Sep 1999

Conference

Conference5th European Conference on Planning (ECP 99)
CityDurham, England
Period8/09/9910/09/99

Keywords

  • linear logic
  • planning systems

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

Cite this