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.
|Number of pages||13|
|Publication status||Published - 8 Sep 1999|
|Event||5th European Conference on Planning (ECP 99) - Durham, England|
Duration: 8 Sep 1999 → 10 Sep 1999
|Conference||5th European Conference on Planning (ECP 99)|
|Period||8/09/99 → 10/09/99|
- linear logic
- planning systems
Cresswell, S., Smaill, A., & Richardson, J. (1999). Deductive synthesis of recursive plans in linear logic. 252-264. Paper presented at 5th European Conference on Planning (ECP 99), Durham, England, .