Computer Science – Programming Languages
Scientific paper
2001-02-23
Computer Science
Programming Languages
39 pages, 5 figures. To appear in Theory and Practice of Logic Programming
Scientific paper
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 that consists of the language LO 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. 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 for an interesting class of LO programs encoding Petri Nets.
Bozzano Marco
Delzanno Giorgio
Martelli Maurizio
No associations
LandOfFree
An Effective Fixpoint Semantics for Linear Logic Programs does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with An Effective Fixpoint Semantics for Linear Logic Programs, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and An Effective Fixpoint Semantics for Linear Logic Programs will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-465707