A Model-Theoretic Reconstruction of the Operational Semantics of Logic Programs

AbstractIn 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 operational semantics are all models. An ordering on interpretations is defined to overcome the problem that the intersection of a set of models is not necessarily a model. 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 a model. Thus there exists a least model, which is the least Herbrand model and therefore the ground success set semantics. Richer operational semantics are non-least models, which can, however, be effectively defined by fixpoint constructions. The model corresponding to the computed answer substitutions operational semantics is the most primitive one (the others can easily be obtained from it)