Deductive synthesis of recursive plans in linear logic

Stephen Cresswell; Alan Smaill; Julian Richardson

Deductive synthesis of recursive plans in linear logic

Stephen Cresswell, Alan Smaill, Julian Richardson

Computer And Information Sciences

Research output: Contribution to conference › Paper › peer-review

34 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 language	English
Pages	252-264
Number of pages	13
Publication status	Published - 8 Sept 1999
Event	5th European Conference on Planning (ECP 99) - Durham, England Duration: 8 Sept 1999 → 10 Sept 1999

Conference

Conference	5th European Conference on Planning (ECP 99)
City	Durham, England
Period	8/09/99 → 10/09/99

Keywords

linear logic
planning systems

Access to Document

strathprints001952Accepted author manuscript, 212 KB

Cite this

@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 = sep,

day = "8",

language = "English",

pages = "252--264",

note = "5th European Conference on Planning (ECP 99) ; Conference date: 08-09-1999 Through 10-09-1999",

}

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

T2 - 5th European Conference on Planning (ECP 99)

Y2 - 8 September 1999 through 10 September 1999

ER -

Deductive synthesis of recursive plans in linear logic

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this