Information Services banner Edinburgh Research Archive The University of Edinburgh crest

Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1842/1896

This item has been viewed 13 times in the last year. View Statistics

Files in This Item:

File Description SizeFormat
cresswell_thesis.pdf867.95 kBAdobe PDFView/Open
Title: Deductive synthesis of recursive plans in linear logic
Authors: Creswell, Stephen N
Supervisor(s): Smaill, Alan
Richardson, Julian
Issue Date: 2001
Abstract: Conventionally, the problem of plan formation in Artificial Intelligence deals with the generation of plans in the form of a sequence of actions. This thesis describes an approach to extending the expressiveness of plans to include conditional branches and recursion. This allows problems to be solved at a higher level, such that a single plan in such a language is capable of solving a class of problems rather than a single problem instance. A plan of fixed size may solve arbitrarily large problem instances. To form such plans, we take a deductive planning approach, in which the formation of the plan goes hand-in-hand with the construction of the proof that the plan specification is realisable. The formalism used here for specifying and reasoning with planning problems is Girard's Institutionistic Linear Logic (ILL), which is attractive for planning problems because state change can be expressed directly as linear implication, with no need for frame axioms. We extract plans by means of the relationship between proofs in ILL and programs in the style of Abramsky. We extend the ILL proof rules to account for induction over inductively defined types, thereby allowing recursive plans to be synthesised. We also adapt Abramsky's framework to partially evaluate and execute the plans in the extended language. We give a proof search algorithm tailored towards the fragment of the ILL employed (excluding induction rule selection). A system implementation, Lino, comprises modules for proof checking, automated proof search, plan extraction and partial evaluation of plans. We demonstrate the encodings and solutions in our framework of various planning domains involving recursion. We compare the capabilities of our approach with the previous approaches of Manna and Waldinger, Ghassem-Sani and Steel, and Stephen and Biundo. We claim that our approach gives a good balance between coverage of problems that can be described and the tractability of proof search.
Description: Centre for Intelligent Systems and their Applications
Sponsor(s): Engineering and Physical Sciences Research Council (EPSRC)
Keywords: computer science
artificial intelligence
URI: http://hdl.handle.net/1842/1896
Appears in Collections:Informatics thesis and dissertation collection

Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.

 

Valid XHTML 1.0! Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh 2013, and/or the original authors. Privacy and Cookies Policy