Semantics of infinite tree logic programming. (English) Zbl 0621.68054

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. 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 in any (possibly infinite) P-derivation is solvable iff each of its finite stumps is solvable. This is true for programs containing no inequations, but is false for the program Q above.
Reviewer: G.Mints


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68N01 General topics in the theory of software


Zbl 0547.68005
Full Text: DOI


[1] Abdalluh, M., Metric interpretation and greatest fixpoint semantics of logic programs, ()
[2] Colmerauer, A., Prolog and infinite trees, (), 231-251
[3] Colmerauer, A., PROLOG II—reference manual and theoretical model, ()
[4] Colmerauer, A., Equations and unequations on finite and infinite trees, (), 85-99
[5] Colmerauer, A., Equations et inequations sur LES arbres finis et infinis, ()
[6] Courcelle, B., Fundamental properties of infinite trees, Theoret. comput. sci., 25, 2, 95-169, (1983) · Zbl 0521.68013
[7] Van Emden, M.H.; Kowalski, R.A., The semantics of predicate logic as a programming language, J. ACM, 23, 4, 733-742, (1976) · Zbl 0339.68004
[8] Van Emden, M.H.; Lloyd, J.W., A logical reconstruction of prolog II, (), 35-40 · Zbl 0594.68033
[9] Jaffar, J.; Lassez, J.-L.; Maher, M.J., A logical foundation for PROLOG II, ()
[10] Jaffar, J.; Lassez, J.-L.; Maher, M.J., A theory of complete logic programs with equality, J. logic programming, 1, 3, 211-223, (1984) · Zbl 0584.68021
[11] Jaffar, J.; Lassez, J.-L.; Maher, M.J., A logic programming language scheme, () · Zbl 0547.68034
[12] Kanoui, H., PROLOG II—manual of examples, ()
[13] Lloyd, J.W., Foundations of logic programming, (1984), Springer Berlin · Zbl 0547.68005
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.