On Resolution in Fragments of Classical Linear Logic (Extended Abstract)
J A Harland and D J PymAbstract: We present a proof-theoretic foundation for logic programming in Girard's linear logic. We exploit the permutability properties of two-sided linear sequent calculus to identify appropriate notions of uniform proof, definite formula, goal formula, clause and resolution proof for fragments of linear logic. The analysis of this paper extends earlier work by the present authors to include negative occurrences of "+" (par) and positive occurrences of ! (of course !) and ? (why not ?). These connectives introduce considerable difficulty. We consider briefly some of the issues related to the mechanical implementation of our resolution proofs.
Previous | Index | Next