A Hierarchy of Semantics for Normal Constraint Logic Programs

The different properties characterizing the operational behavior of logic programs can be organized in a hierarchy of fixpoint semantics related by Galois insertions, having the least Herbrand model as most abstract semantics, and the SLD operational semantics as most concrete semantics. The choice of a semantics in the hierarchy allows to model precisely the program properties of interest while getting rid of useless details of too concrete semantics, which is crucial for the development of efficient program analysis tools. The aim of this paper is to push forward these methods by making them apply to normal (constraint) logic programs, that is full first-order (non Horn) programs. The fixpoint semantics defined by the first author for the rule of constructive negation by pruning is at the center of the hierarchy developed in this paper. We show that that semantics can be obtained by concretization of Kunen's semantics defined as a fixpoint, taken as the most abstract semantics of the hierarchy, and that by further concretization it leads to a new operational semantics for normal CLP programs. The different observable properties of the program, such as successful derivations, finite failure, set of computed answer constraints, etc. are modeled by precise semantics in the hierarchy.