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 Bottom-up abstract interpretation of logic programs

1994 ◽  
Vol 124 (1) ◽  
pp. 93-125 ◽  
Author(s):  
Michael Codish ◽  
Dennis Dams ◽  
Eyal Yardeni
Keyword(s):  
Abstract Interpretation ◽  
Logic Programs ◽  
Bottom Up

scholarly journals Optimality in goal-dependent analysis of Sharing

2009 ◽  
Vol 9 (05) ◽  
pp. 617-689 ◽  
Author(s):  
GIANLUCA AMATO ◽  
FRANCESCA SCOZZARI
Keyword(s):  
Logic Programming ◽  
Static Analysis ◽  
Abstract Interpretation ◽  
Logic Programs ◽  
Semantic Operators

AbstractWe face the problems of correctness, optimality, and precision for the static analysis of logic programs, using the theory of abstract interpretation. We propose a framework with a denotational, goal-dependent semantics equipped with two unification operators for forward unification (calling a procedure) and backward unification (returning from a procedure). The latter is implemented through a matching operation. Our proposal clarifies and unifies many different frameworks and ideas on static analysis of logic programming in a single, formal setting. On the abstract side, we focus on the domainsharingby Jacobs and Langen (The Journal of Logic Programming, 1992, vol. 13, nos. 2–3, pp. 291–314) and provide the best correct approximation of all the primitive semantic operators, namely, projection, renaming, and forward and backward unifications. We show that the abstract unification operators are strictly more precise than those in the literature defined over the same abstract domain. In some cases, our operators are more precise than those developed for more complex domains involving linearity and freeness.

RECOGNIZING NON-FLOUNDERING LOGIC PROGRAMS AND GOALS

1990 ◽  
Vol 01 (02) ◽  
pp. 151-163 ◽  
Author(s):  
ROBERTO BARBUTI ◽  
MAURIZIO MARTELLI
Keyword(s):  
Logic Programming ◽  
Abstract Interpretation ◽  
Logic Programs ◽  
Negation As Failure ◽  
Proof Procedure ◽  
Resolution Proof

The introduction of negation in Logic Programming using the Negation as Failure Rule causes some problems regarding the completeness of the SLDNF-Resolution proof procedure. One of the causes of incompleteness arises when evaluating a non-ground negative literal. This is solved by forbidding these evaluations. Obviously, there is the possibility of having only non-ground negative literals in the goal (the floundering of the goal). There is a class of programs and goals (allowed) that has been proved to have the non-floundering property. In this paper an algorithm is proposed which recognizes a wider class of programs with this property and which is based on abstract interpretation techniques.

Efficient bottom-up execution of logic programs using abstract interpretation

1993 ◽  
Vol 47 (3) ◽  
pp. 149-157
Author(s):  
Byeong-Mo Chang ◽  
Kwang-Moo Choe ◽  
Taisook Han
Keyword(s):  
Abstract Interpretation ◽  
Logic Programs ◽  
Bottom Up

Topological Model Set Deformations in Logic Programming

1989 ◽  
Vol 12 (3) ◽  
pp. 357-399
Author(s):  
Aida Batarekh ◽  
V.S. Subrahmanian
Keyword(s):  
Logic Programming ◽  
Sufficient Conditions ◽  
Topological Spaces ◽  
Logic Programs ◽  
First Order ◽  
Order Language ◽  
Language L ◽  
General Logic ◽  
Model Set ◽  
Necessary And Sufficient

Given a first order language L, and a notion of a logic L w.r.t. L, we investigate the topological properties of the space of L-structures for L. We show that under a topology called the query topology which arises naturally in logic programming, the space of L-models (where L is a decent logic) of any sentence (set of clauses) in L may be regarded as a (closed, compact) T4-space. We then investigate the properties of maps from structures to structures. Our results allow us to apply various well-known results on the fixed-points of operators on topological spaces to the semantics of logic programming – in particular, we are able to derive necessary and sufficient topological conditions for the completion of covered general logic programs to be consistent. Moreover, we derive sufficient conditions guaranteeing the consistency of program completions, and for logic programs to be determinate. We also apply our results to characterize consistency of the unions of program completions.

scholarly journals Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLP

2019 ◽  
Vol 19 (5-6) ◽  
pp. 1107-1123
Author(s):  
JOAQUÍN ARIAS ◽  
MANUEL CARRO
Keyword(s):  
Logic Programming ◽  
Abstract Interpretation ◽  
Constraint Logic Programming ◽  
Additional Cost ◽  
Logic Programs ◽  
Semantic Equivalence ◽  
Constraint Solver ◽  
Abstract Domains ◽  
Interpretation Algorithm ◽  
Branch Switching

AbstractCiaoPP is an analyzer and optimizer for logic programs, part of the Ciao Prolog system. It includes PLAI, a fixpoint algorithm for the abstract interpretation of logic programs which we adapt to use tabled constraint logic programming. In this adaptation, the tabling engine drives the fixpoint computation, while the constraint solver handles the LUB of the abstract substitutions of different clauses. That simplifies the code and improves performance, since termination, dependencies, and some crucial operations (e.g., branch switching and resumption) are directly handled by the tabling engine. Determining whether the fixpoint has been reached uses semantic equivalence, which can decide that two syntactically different abstract substitutions represent the same element in the abstract domain. Therefore, the tabling analyzer can reuse answers in more cases than an analyzer using syntactical equality. This helps achieve better performance, even taking into account the additional cost associated to these checks. Our implementation is based on the TCLP framework available in Ciao Prolog and is one-third the size of the initial fixpoint implementation in CiaoPP. Its performance has been evaluated by analyzing several programs using different abstract domains.

Sign in / Sign up

Export Citation Format

Share Document