Declarative modeling of the operational behavior of logic languages

The paper defines a new declarative semantics for logic programs, which is based on interpretations containing (possibly) non-ground atoms. Two different interpretations are introduced and the corresponding models are defined and compared. The classical results on the Herbrand model semantics of logic programs are shown to hold in the new models too (i.e. existence of a minimal model, fixpoint characterization, etc.). With the new models, we have a stronger soundness and completeness result for SLD-resolution. In particular, one of the two models allows the set of computed answer substitutions to be characterized precisely.