Abstract

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