zbMATH — the first resource for mathematics

Foundations of deductive databases and logic programming. (English) Zbl 0726.68064
Los Altos, CA: Morgan Kaufmann Publishers. 746 p. £29.95 (1988).
[For the entire collection see Zbl 0699.68009)]. The paper discusses a generalization of the concept of hierarchical constraints, the class of stratified logic programs and databases and propose a semantics for negation that combines the approach of the generalized closed world assumption with that of completed databases. A deductive database that consists of a set of clauses is stratified if the clauses can be partioned into ordered sets of clauses such that if a negated atom appears in the body of a clause in a partition, then the definition of the atom appears in a previous partition, and if a positive atom appears in the body of a clause, then its definition appears either in the same partition or in a previous partition. Whether a given program is stratified can be tested by dependency graphs. Programs in this class have a simple declarative and procedural meaning based, respectively, on model theory and a back-chaining interpreter. The authors develop the fixpoint theory of nonmonotonic operators and apply it to provide a declarative meaning of a general program. Models of a program are not only minimal but also supported, i.e., a ground atom is true if there is a ground instance of a clause of the program with the ground clause as its head and a body which is true. A stratified program has a unique intended model. Stratified programs have minimal models which are also a model of the completion of the program that proves the consistency of the completed model database for stratified programs. For a stratified program the definition of the interpreter uniquely specifies which ground atoms are provable from the program.

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68N17 Logic programming