An Effective Bottom-Up Semantics for First-Order Linear Logic Programs

2001 ◽  
pp. 138-152 ◽  
Author(s):  
Marco Bozzano ◽  
Giorgio Delzanno ◽  
Maurizio Martelli
Keyword(s):  
Linear Logic ◽  
Logic Programs ◽  
Bottom Up ◽  
Order Linear ◽  
First Order

scholarly journals On structuring proof search for first order linear logic

2006 ◽  
Vol 360 (1-3) ◽  
pp. 42-76 ◽  
Author(s):  
Paola Bruscoli ◽  
Alessio Guglielmi
Keyword(s):  
Linear Logic ◽  
Order Linear ◽  
First Order ◽  
Proof Search

scholarly journals An effective fixpoint semantics for linear logic programs

2001 ◽  
Vol 2 (1) ◽  
pp. 85-122 ◽  
Author(s):  
MARCO BOZZANO ◽  
GIORGIO DELZANNO ◽  
MAURIZIO MARTELLI
Keyword(s):  
Logic Programming ◽  
Petri Nets ◽  
Abstract Interpretation ◽  
Theoretical Foundation ◽  
Linear Logic ◽  
Sufficient Conditions ◽  
Logic Programs ◽  
Bottom Up ◽  
Interesting Class ◽  
Fixpoint Semantics

In this paper we investigate the theoretical foundation of a new bottom-up semantics for linear logic programs, and more precisely for the fragment of LinLog (Andreoli, 1992) that consists of the language LO (Andreoli & Pareschi, 1991) enriched with the constant 1. We use constraints to symbolically and finitely represent possibly infinite collections of provable goals. We define a fixpoint semantics based on a new operator in the style of TP working over constraints. An application of the fixpoint operator can be computed algorithmically. As sufficient conditions for termination, we show that the fixpoint computation is guaranteed to converge for propositional LO. To our knowledge, this is the first attempt to define an effective fixpoint semantics for linear logic programs. As an application of our framework, we also present a formal investigation of the relations between LO and Disjunctive Logic Programming (Minker et al., 1991). Using an approach based on abstract interpretation, we show that DLP fixpoint semantics can be viewed as an abstraction of our semantics for LO. We prove that the resulting abstraction is correct and complete (Cousot & Cousot, 1977; Giacobazzi & Ranzato, 1997) for an interesting class of LO programs encoding Petri Nets.

scholarly journals First-order linear logic without modalities is NEXPTIME-hard

1994 ◽  
Vol 135 (1) ◽  
pp. 139-153 ◽  
Author(s):  
P. Lincoln ◽  
A. Scedrov
Keyword(s):  
Linear Logic ◽  
Order Linear ◽  
First Order
Sign in / Sign up

Export Citation Format

Share Document