The Uniform Proof-Theoretic Foundation of Linear Logic Programming
James Harland and David PymAbstract: We present a theory of logic programming for Girard's linear logic. In the spirit of recent work of Miller et al., we identify suitable classes of definite formulae and goal formulae by considering classes of formulae that resemble the Harrop formulae of intuitionistic first-order logic. We isolate the appropriate notion of uniform proof in linear logic, and show that this characterizes resolution proofs. Resolution proofs in linear logic are somewhat difficult to define. This difficulty arises from the need to decompose definite formulae into a form suitable for the use of the linear resolution rule, a rule which requires the clause selected to be deleted after use.
We provide an elementary quantale semantics for our logic programs and give an appropriate completeness theorem.
We consider a translation - resembling those of Girard - of the intuitionistic hereditary Harrop formulae and intuitionistic uniform proofs into our framework, and show that certain properties are preserved under this translation.
Previous | Index | Next