Deductive synthesis of recursive plans in linear logic

Stephen Cresswell, Alan Smaill, Julian Richardson

Research output: Contribution to conferencePaperpeer-review

21 Downloads (Pure)


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


Conference5th European Conference on Planning (ECP 99)
CityDurham, England


  • linear logic
  • planning systems


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

Cite this