A model-theoretic reconstruction of the operational semantics of logic programs (Q1803658)

This paper shows the relations between various models for logic programming, and compare their relative capability to capture features of the operational semantics. The main novelty consists of considering Herbrand interpretations with variables, based on which a new notion of truth is defined, which extends the classical one. The model thus defined is shown to characterize the set of the computed answer substitutions, and it is ``the most informative'' in this framework. Other models, corresponding to the ground success set, and to the atomic consequences set, are shown to be derivable from the former. The relation of ``containing more information'' is captured by an appropriate ordering on sets of atoms (interpretations). All these models are shown to be the fixpoints of suitable one-step consequence operators.