Deductive synthesis of recursive plans in linear logic

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.