On the Relations between Disjunctive and Linear Logic Programming

In this paper we investigate the relationship between Disjunctive Logic Programming as defined in [13] and a subset of Linear Logic, namely the fragment of LinLog [2] which corresponds to Andreoli and Pareschi's LO [3]. We analyze the two languages both from a top-down, operational perspective, and from a bottom-up, semantical one. From a proof-theoretical perspective, we show that, modulo a simple mapping between classical and linear connectives, LO can be viewed as a sub-structural fragment of DLP in which the rule of contraction is forbidden on the right-hand side of sequents. We also prove that LO is strictly more expressive than DLP in the propositional case. From a semantical perspective, after recalling the definition of a bottom-up fixpoint semantics for LO we have given in our previous work [5], we show that DLP fixpoint semantics can be viewed as an abstraction of the corresponding LO semantics, defined over a suitable abstract domain. We prove that the abstraction is correct and complete in the sense of [6,8]. Finally, we show that the previous property of the semantics is strictly related to proof-theoretical properties of the classical and linear logic fragments underlying DLP and LO.