Graph properties for normal logic programs

The completion of a program introduced by Clark is important for giving a declarative semantics to the negation as failure rule and to SLDNF resolution. Essential for having a completeness result is the consistency of the completion. The aim of this work is to give a unifying presentation of several known classes of programs that have consistent completion. The consistency of the completion of a program P is guaranteed by some properties of the graph which represents the dependency relation between the predicate symbols of P (global dependencies), or the ground atoms of the Herbrand basis of P (local dependencies). A taxonomy of program classes which are discriminated by these properties is presented, together with a uniform presentation of the (mostly well-known) techniques of model construction for the programs of each class. In this perspective it is also easier to understand the concept of perfect model and the relation between models of the completion and circumscription. © 1993