Towards a logical semantics for pure Prolog

The coincidence of the declarative and procedural interpretations of logic programs does not apply to Prolog programs, due to the depth-first left-to-right evaluation strategy of Prolog interpreters. We propose a semantics for Prolog programs based on a four-valued logic. The semantics is based on a new concept of completion analogous to Clarkʹs and it enjoys the nice properties of the declarative semantics of logic programming: existence of the least Herbrand model, equivalence of the model-theoretic and operational semantics.