Which formal system provides the semantic foundation for Prolog ?

Answer: Predicate calculus (first-order predicate logic) is the semantic foundation for Prolog.

• Model-theoretic semantics: The meaning of a Prolog program is given by its models. In practice the Herbrand universe, Herbrand base and Herbrand interpretations are used, and the least Herbrand model captures the declarative meaning of the program.

• Fixpoint semantics: The immediate consequence operator (often written T_P) characterizes program consequences; the least fixpoint of this operator corresponds to the least Herbrand model.

• Proof-theoretic / Operational semantics: SLD-resolution is the proof/search procedure used by Prolog. It is designed to be sound and (under appropriate conditions) complete with respect to the declarative (model-theoretic) semantics.

Why the other systems are not the semantic foundation:

• Lambda calculus provides a foundation for functional computation and higher-order functions, not the logic-based semantics Prolog uses.

• Hoare logic is for reasoning about correctness of imperative programs via assertions; it is not a model-theoretic foundation for logic programming.

• Propositional logic lacks quantifiers and the expressive power to represent relations over objects, which first-order predicate logic provides and which Prolog relies on.