In this paper we 1. provide a natural deduction system for full first-order linear logic, 2. introduce Curry-Howard-style terms for this version of linear logic, 3. extend the notion of substitution of Curry-Howard terms for term variables, 4. define the reduction rules for the Curry-Howard terms and 5. outline a proof of the strong normalization for the full system of linear logic using a development of Girard's candidates for reducibility, thereby providing an alternative to Girard's proof using proof-nets.

Cerrito has proposed a declarative semantics for allowed logic programs using Girard's linear logic, with weakening. We propose an alternative semantics using pure linear logic. The main difference between our approach and that of Cerrito is that the comma of a logic program is interpreted as the multiplicative connective instead of the additive &. This enables us to establish a soundness result without the introduction of the projection symbols employed by Cerrito. The price to be paid for this simplification occurs (...) in the establishment of a completeness result. Our definition of the completed program is more complicated than that given by Cerrito. We establish a completeness result for the class of allowed programs and queries using our definition of the program completion. (shrink)