Syntax and semantics of logic programming

This article describes the syntax and semantics of the purely declarative subset of these languages.

The syntax and semantics of other logic programming languages are extensions and generalizations of those of Datalog.

[1] If constant and variable are two countable sets of constants and variables respectively and relation is a countable set of predicate symbols, then the following BNF grammar expresses the structure of a Datalog program: Atoms are also referred to as literals.

For example, the following rule is a fact: Many implementations of logic programming extend the above grammar to allow writing facts without the :-, like so: Many also allow writing 0-ary relations without parentheses, like so: These are merely abbreviations (syntactic sugar); they have no impact on the semantics of the program.

There are three widely-used approaches to the semantics of Datalog programs: model-theoretic, fixed-point, and proof-theoretic.

This map T is monotonic with respect to the partial order given by subset inclusion on T. By the Knaster–Tarski theorem, this map has a least fixed point; by the Kleene fixed-point theorem the fixed point is the supremum of the chain

[5] The fixpoint semantics suggest an algorithm for computing the minimal Herbrand model: Start with the set of ground facts in the program, then repeatedly add consequences of the rules until a fixpoint is reached.

Given a program P, a proof tree of a ground atom A is a tree with a root labeled by A, leaves labeled by ground atoms from the heads of facts in P, and branches with children

A top-down reading of the proof trees described above suggests an algorithm for computing the results of such queries, such a reading informs the SLD resolution algorithm, which forms the basis for the evaluation of Prolog.

[7] While the name "logic programming" is used to refer to the entire paradigm of programming languages including Datalog and Prolog, when discussing formal semantics, it generally refers to an extension of Datalog with function symbols.

Logic programming as discussed in this article is closely related to the "pure" or declarative subset of Prolog.

[8] Due to the presence of function symbols, the Herbrand models of logic programs can be infinite.

However, the semantics of a logic program is still defined to be its minimal Herbrand model.

However, any ground atom in the minimal Herbrand model will have a finite proof tree.

In contrast, there are many conflicting proposals for the semantics of logic programs with negation.

Many implementations of Datalog use a bottom-up evaluation model inspired by the fixed point semantics.

Intuitively, stable models are the "possible sets of beliefs that a rational agent might hold, given [the program]" as premises.

Several other extensions of Datalog have been proposed and studied, including variants with support for integer constants and functions (including DatalogZ),[12][13] inequality constraints in the bodies of rules, and aggregate functions.

Hasse diagram of Herbrand interpretations of the Datalog program 
e(x, y).
e(y, z).
p(A, B) :-
  e(A, B).
p(A, C) :- 
  p(A, B),
  e(B, C).
The interpretation is the minimal Herbrand model. All interpretations above it are also models, all interpretations below it are not models.
Proof tree showing the derivation of the ground atom path(x, z) from the program 
edge(x, y).
edge(y, z).
path(A, B) :- 
  edge(A, B).
path(A, C) :- 
  path(A, B), 
  edge(B, C).