Canonical Proofs for Linear Logic Programming Frameworks.
Didier Galmiche · 1994
We discuss here the proof-theoretic foundations for theorem proving and logic programming in linear logic, mainly studying how to define canonical proofs (that are complete) for efficient proof search in fragments of linear logic. We analyze the conception of such proof forms, for frameworks based on proof-construction as computation, emphasizing the relationship between the logical fragment and its proof search strategies. This point is essential for the definition and implementation of logic programming languages within linear logic.