Classical AI Planning as Theorem Proving: The Case of a Fragment of Linear Logic

Contents

This paper attempts to evaluate the use of a theorem prover in the multiplicative fragmeut of linear logic which has been shown to simulate conjunctive STRiPs-like planning. A proof search procedure is presented that is correct, complete and only generates lit,ear proofs (i.e. not trees). Plans that can be extracted from proofs are either totally or partially ordered. The procedure is tested against STRips-like planners and results are given. However, since linear logic is a resource-sensitive logic viewing formulas data types, partial description of the final situation are impossible in linear logic; and shared postconditions are impossible in the fragment presented here. It is then argued that these restrictions eventually makes the presented fragment of linear logic, despite its formal framework, somewhat useless for practical planning purposes.