Deductive synthesis of recursive plans in linear logic

Stephen Cresswell, Alan Smaill, Julian Richardson

Research output: Contribution to conferencePaper

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.
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

Fingerprint

Planning

Keywords

  • linear logic
  • planning systems

Cite this

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, .
Cresswell, Stephen ; Smaill, Alan ; Richardson, Julian. / Deductive synthesis of recursive plans in linear logic. Paper presented at 5th European Conference on Planning (ECP 99), Durham, England, .13 p.
@conference{afd41382beaf47ee8c904ef39c85a72f,
title = "Deductive synthesis of recursive plans in linear logic",
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.",
keywords = "linear logic, planning systems",
author = "Stephen Cresswell and Alan Smaill and Julian Richardson",
year = "1999",
month = "9",
day = "8",
language = "English",
pages = "252--264",
note = "5th European Conference on Planning (ECP 99) ; Conference date: 08-09-1999 Through 10-09-1999",

}

Cresswell, S, Smaill, A & Richardson, J 1999, 'Deductive synthesis of recursive plans in linear logic' Paper presented at 5th European Conference on Planning (ECP 99), Durham, England, 8/09/99 - 10/09/99, pp. 252-264.

Deductive synthesis of recursive plans in linear logic. / Cresswell, Stephen; Smaill, Alan; Richardson, Julian.

1999. 252-264 Paper presented at 5th European Conference on Planning (ECP 99), Durham, England, .

Research output: Contribution to conferencePaper

TY - CONF

T1 - Deductive synthesis of recursive plans in linear logic

AU - Cresswell, Stephen

AU - Smaill, Alan

AU - Richardson, Julian

PY - 1999/9/8

Y1 - 1999/9/8

N2 - 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.

AB - 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.

KW - linear logic

KW - planning systems

M3 - Paper

SP - 252

EP - 264

ER -

Cresswell S, Smaill A, Richardson J. Deductive synthesis of recursive plans in linear logic. 1999. Paper presented at 5th European Conference on Planning (ECP 99), Durham, England, .