Fixpoint semantics for logic programming a survey

This paper defines a new concurrent logic language, Nested Guarded Horn Clauses (NGHC). The main new feature of the language is its concept of guard. In fact, an NGHC clause has several layers of (standard) guards. This syntactic innovation allows the definition of a complete (i.e. always applicable) set of unfolding rules and therefore of an unfolding semantics which is equivalent, with respect to the success set, to the operational semantics. A fixpoint semantics is also defined in the classic logic programming style and is proved equivalent to the unfolding one. Since it is possible to embed Flat GHC into NGHC, our method can be used to give a fixpoint semantics to FGHC as well.

Download Full-text

On Greatest Fixpoint Semantics of Logic Programming

Journal of Logic and Computation ◽

10.1093/logcom/12.2.321 ◽

2002 ◽

Vol 12 (2) ◽

pp. 321-342 ◽

Cited By ~ 3

Author(s):

M. Jaume

Keyword(s):

Logic Programming ◽

Fixpoint Semantics

Download Full-text

A Denotational Semantics for Logic Programming

DAIMI Report Series ◽

10.7146/dpb.v14i201.7552 ◽

1985 ◽

Vol 14 (201) ◽

Cited By ~ 1

Author(s):

Gudmund Skovbjerg Frandsen

Keyword(s):

Logic Programming ◽

Logic Program ◽

Denotational Semantics ◽

Power Domain ◽

Fixpoint Semantics ◽

Standard Domain

A fully abstract denotational semantics for logic programming has not been constructed yet. In this paper we present a denotational semantics that is almost fully abstract. We take the meaning of a logic program to be an element in a Plotkin power domain of substitutions. In this way our result shows that standard domain constructions suffice, when giving a semantics for logic programming. Using the well-known fixpoint semantics of logic programming we have to consider two different fixpoints in order to obtain information about both successful and failed computations. In contrast, our semantics is uniform in that the (single) meaning of a logic program contains information about both successful, failed and infinite computations. Finally, based on the full abstractness result, we argue that the detail level of substitutions is needed in any denotational semantics for logic programming.

Download Full-text

Fair Derivations in Logic Programming: Operational and Greatest Fixpoint Semantics

Fundamenta Informaticae ◽

10.3233/fi-1987-10303 ◽

1987 ◽

Vol 10 (3) ◽

pp. 247-307

Author(s):

Mohand-Areski Nait Abdallah

Keyword(s):

Logic Programming ◽

Topological Methods ◽

Soundness And Completeness ◽

Fix Point ◽

Fixpoint Semantics ◽

Uniform Treatment

Using topological methods, we study the operational and greatest fixpoint semantics of infinite computations in logic programming. We show the equivalence of the operational and greatest fix point semantics in the case of fair derivations. We give some canonical partition, and soundness and completeness results which generalize already known results about the finitary case. Since fair derivations are a generalization of successful derivations, we thus give a uniform treatment of all meaningful computations in logic programming.

Download Full-text

An effective fixpoint semantics for linear logic programs

Theory and Practice of Logic Programming ◽

10.1017/s1471068402001254 ◽

2001 ◽

Vol 2 (1) ◽

pp. 85-122 ◽

Cited By ~ 9

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.

Download Full-text