Project: Plans from proofs

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.