Semantics of infinite tree logic programming
type: Item
instance of: scholarly article
title: Semantics of infinite tree logic programming
zbMATH Open document ID: 0621.68054
DOI: 10.1016/0304-3975(86)90027-7
author: Joxan Jaffar
author: Peter J. Stuckey
published in: Theoretical Computer Science
publication date: 1986-01-01T00:00:00Z
review text: The logic programs considered here consist of clauses \(A\leftarrow S[ ]B\), where A is an atom, B is a finite sequence of atoms and S is a finite sequence of equations and inequations. Unification is made as in PROLOG, i.e. without ''occurs check'', so f(x) and x are unifiable and the result is the infinite term f(f(...)). The main difference from the treatment in the literature [cf. \textit{J. W. Lloyd}, Foundations of logic programming (1984; Zbl 0547.68005)] concerns inequalities. The equation (resp. inequation) of terms u, v is true for a substitution s if us, vs coincide (resp. do not coincide). A satisfier of a system S of equations and inequations is a substitution s such that any element of S is true under any ground instance of s. Derivation sequences, success set SS(P), finite failure set FF(P), immediate consequence function \(T_ p\) for a program P are defined in a familiar way. In the absence of inequations \(T_ p\) is continuous in Baire topology on infinite terms and atoms containing such terms, but for the program \(Q=\{p(x)\leftarrow (x=a[ ]q(y));q(x)\leftarrow (x=f(y),x\neq f(x)[ ]q(y))\}\), the \(T_ Q\) is discontinuous at q(f(f(...))). So, instead of simply considering closed Herbrand interpretations to prove standard results on fixed points, the authors have to check that the results of T-operations have rational cover: any ground atom in a set is an instance of a rational atom (having only a finite number of subterms). This turns out to be possible since unification (without the occurs check) preserves rationality and any finite system S having ground satisfier s, has also a rational satisfier s'\(\geq s\). Defining a (Clark-)completed program \(P^*\) for a program P in the usual way, the authors prove that \(P^*\vDash A\) iff A belongs to SS(P). Here \(\vDash\) means consequence in all Herbrand models. Similar equivalence for \(\sim A\) and FF(P) holds exactly when P is derivation compact: the sequence S' of equations and inequations arising …
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68N01
zbMATH DE Number: 4007748
zbMATH Keywords: semantics
zbMATH Keywords: infinite tree logic programming
zbMATH Keywords: PROLOG
zbMATH Keywords: inequalities
zbMATH Keywords: satisfier
zbMATH Keywords: unification
zbMATH Keywords: completed program
zbMATH Keywords: consequence in all Herbrand models
Wikidata QID: Q55921413
reviewed by: G. E. Mints
MaRDI profile type: Publication
full work available at URL: 0304-3975(86)90027-7
OpenAlex ID: W2091154692
cites work: Fundamental properties of infinite trees
cites work: The Semantics of Predicate Logic as a Programming Language
cites work: A logical reconstruction of Prolog II
cites work: A theory of complete logic programs with equality
cites work: Closures and fairness in the semantics of programming logic
cites work: Q3339245
Recommended article: Q3221399
Recommended article: Toward a declarative semantics for infinite objects in logic programming
Recommended article: Logic programming with infinite sets
Recommended article: Q4029601
Recommended article: Q3998008
Recommended article: Prolog infinite trees and automata
Recommended article: Q3221429
Recommended article: Infinitary logic for computer science
Recommended article: Q4708939
Recommended article: Extended Computation Tree Logic
description: scientific article; zbMATH DE number 4007748