In this paper we investigate the relationship between Disjunctive Logic Programming as defined in  and a subset of Linear Logic, namely the fragment of LinLog  which corresponds to Andreoli and Pareschi's LO . 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 , 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.
|Titolo:||On the Relations between Disjunctive and Linear Logic Programming|
|Data di pubblicazione:||2001|
|Appare nelle tipologie:||1.1 Articolo in rivista|