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.

On the Relations between Disjunctive and Linear Logic Programming

Marco Bozzano;
2001

Abstract

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.
File in questo prodotto:
File Dimensione Formato  
entcs01.pdf

accesso aperto

Tipologia: Documento in Post-print
Licenza: DRM non definito
Dimensione 321.01 kB
Formato Adobe PDF
321.01 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11582/328068
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
social impact