A Model-Theoretic Reconstruction ofthe Operational Semantics of Logic Programs

In this paper we define a new notion or truth on Herbrand interpretations extended with variables which allows us to capture, by means of suitable models, various observable properties, such as the ground success set, the set of atomic consequences, and the computed answer substitutions. The notion of truth extends the classical one to account for non-ground formulas in the interpretations. The various operationalsemantics are all models. An ordering on interpretations is defined to overcome the problem that the intersection of a set of models is not necessarily amodel. The set of interpretations with this partial order is shown to be a complete lattice, and the greatest lower bound of any set of models is shown to be amodel. Thus there exists a least model, which is the least Herbrand model and therefore the ground success set semantics. Richer operationalsemantics are non-least models, which can, however, be effectively defined by fixpoint constructions. The model corresponding to the computed answer substitutions operationalsemantics is the most primitive one (the others can easily be obtained from it).