A Better Logical Semantics for Prolog

This paper describes a semantics for the language of pure positive Prolog programs that improves on the widely accepted Least Herbrand Model (LHM) semantics. The LHM semantics gives meaning only to complete Prolog programs, and not to components of programs. Yet programmers clearly understand the meaning of a predicate even if not all predicates used in its definition are defined in the program. For example, programmers understand the meaning of the two rules defining transitive closure without having to know the specific graph that it applies to. A semantics for the Prolog language should also provide such a meaning. We motivate the meaning of Prolog rules as inductive definitions by starting with Clark’s completion, analyzing its limitations, and then describing how it can be modified to yield a logical theory of inductive definitions.