
handle: 11567/205591 , 11582/328068
AbstractIn 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.
004, Theoretical Computer Science, Computer Science(all)
004, Theoretical Computer Science, Computer Science(all)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
