Lucas Dixon →
Teaching →
Project: Plans from proofs

Msc Project by: Guillermo Ivan Gallegos Ayala

Supervisors: Lucas Dixon, Alan Smaill

Plans from proofs -- Guillermo Ivan Gallegos Ayala, Master of Science, School of Informatics, University of Edinburgh, 2005. [PDF, 83 pages]

**Abstract:**

We use the deductive planning approach, by constructing plans from proofs in a se-
quent calculus formalisation of Intuitionistic Linear Logic. There is an essential rela-
tion between the proof terms and the rules of the Logic which is captured by a linear
term assignment. We use the formalization of rules and the linear term assignment
introduced in [A93]. This idea of the assignment of proof terms is then extended from
the rules of the Logic to axioms that are used to solve specific planning problems.
The identification and representation of the necessary axioms, together with the prob-
lem specification is simplified by using the resource oriented style of Linear Logic,
and taking advantage of its expressiveness and simplicity. Expressiveness in this work
does not have its unique manifestation in the Logic but also in the representation of the
proof terms themselves, due to the use of a typed lambda calculus for the linear term
assignment. This characteristic is fairly preserved by Lambda Prolog, the language of
our implementation. Both, the rules of the Logic and the axioms of planning prob-
lems have been implemented as tactics in a system which is based on previous work
described in [F93].

- [F93]: A. Felty. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning, 11(1):43-81, August 1993.
- [A93]: S. Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111:3--57, 1993.