Logic Programming

Origin. Kowalski's "Predicate logic as a programming language" (1974) proposed the procedural interpretation of Horn clauses: read a clause H :- B₁, ..., Bₙ as a procedure declaration whose body is a list of calls, and resolution becomes execution. Colmerauer and Roussel had built the first Prolog at Marseille in 1972 for natural-language processing, and the two strands converged into a declarative programming paradigm. Van Emden and Kowalski (1976) supplied the fixpoint semantics, Clark (1978) added negation as failure and the program completion, and the language was standardized as ISO/IEC 13211-1 (1995).

Models. A program is a logical theory and running it is searching for a proof. The meaning of a definite program is its least Herbrand model, the smallest set of ground atoms closed under the rules, and a query asks for substitutions making a goal true in that model. Computation is goal-directed backward chaining by SLD-resolution, driven by unification rather than by assignment, so the same clause can serve to test, to compute forward, or to compute backward. Negation is not classical: a negative goal succeeds when the positive goal finitely fails, which reads the program as a closed description of the world.

Formalism.

Definite clause: H :- B₁, ..., Bₙ. Head H true if body B₁ ∧ ... ∧ Bₙ true. Universally quantified; exactly one head atom.

Fact: H. Clause with empty body.

Query: ?- G₁, ..., Gₘ. Denial ¬(G₁ ∧ ... ∧ Gₘ); refuting it proves the goals.

Herbrand base: U_P: ground terms from the symbols of P. B_P: ground atoms over U_P. Herbrand interpretation: any I ⊆ B_P.

Immediate consequence operator: T_P(I) = {Hσ : (H :- B) ∈ P, Bσ ground, Bσ ⊆ I} T_P ↑ 0 = ∅, T_P ↑ (n+1) = T_P(T_P ↑ n), T_P ↑ ω = ⋃ₙ T_P ↑ n. M_P = least Herbrand model = lfp(T_P) = T_P ↑ ω.

Unification: Find σ with σ(t₁) = σ(t₂). Most general unifier, unique up to renaming. Occurs check: reject X = f(X).

SLD resolution: Select a goal Gᵢ by the computation rule. Unify Gᵢ with a renamed clause head H. Replace Gᵢ by the body; apply the mgu. Computed answer: the composed substitution restricted to the query.

Negation as failure: not G succeeds if G finitely fails. SLDNF = SLD plus this rule. Completion comp(P): replace :- by ↔ and add equality axioms.

Cut: !: commits to the clause and to the goals solved to its left. Prunes the SLD tree; no declarative reading.

Definite clause grammars: DCG: grammar as logic program with two extra difference-list arguments. Parsing as theorem proving.

Symbols.

Symbol	Unicode	Name	Meaning
∧	U+2227	Conjunction	Body of a clause
¬	U+00AC	Negation	Denial form of a query
⊨	U+22A8	Double turnstile / Entailment	Logical consequence from the program
⊆	U+2286	Subset	Herbrand interpretation inside the Herbrand base
∈	U+2208	Membership	Clause belonging to the program
∅	U+2205	Empty set	Base of the T_P iteration
⋃	U+22C3	N-ary union	Limit stage of the iteration
↔	U+2194	Biconditional	Completion turns each definition into an equivalence
↑	U+2191	Upward arrow / Ordinal power	Stage of the T_P iteration
ω	U+03C9	Omega	Closure ordinal of T_P for definite programs
σ	U+03C3	Sigma / Substitution	Most general unifier, computed answer
!	U+0021	Exclamation mark / Cut	Commits to the current choices
:-	—	Clause arrow	Head holds if body holds
?-	—	Query prefix	Goal to be refuted
,	U+002C	Comma	Conjunction of body literals or goals
not	—	Negation as failure	Succeeds when the goal finitely fails
P	—	Program	The set of clauses
T_P	—	Immediate consequence	One-step closure of an interpretation
M_P	—	Least Herbrand model	Declarative meaning of a definite program
B_P	—	Herbrand base	Ground atoms of the language of P
lfp	—	Least fixpoint	Smallest I with T_P(I) = I
comp(P)	—	Completion	Only-if reading of the program

Metatheory. Van Emden and Kowalski (1976) proved that for a definite program the three natural readings coincide: the ground atoms logically implied by P, the least Herbrand model M_P, and the least fixpoint of the immediate-consequence operator T_P, which is continuous and therefore reaches its fixpoint at stage ω. SLD-resolution is sound and complete for this semantics — every computed answer is a correct answer, and every correct answer is an instance of some computed one — and Apt and van Emden (1982) proved independence of the computation rule, so which goal is selected changes efficiency but not the set of computed answers, while the clause ordering changes only the order in which they arrive. Negation behaves differently. Clark (1978) showed SLDNF sound with respect to the completion comp(P) rather than P itself, and completeness holds only under syntactic restrictions such as stratification or allowedness. With function symbols the Herbrand base is infinite and entailment is only recursively enumerable: logic programming is Turing complete, so termination is undecidable.

Applies to. Prolog. Deductive databases (Datalog). AI planning. Expert systems. Constraint logic programming. Natural language parsing. Program analysis.

Limitations. Prolog's fixed strategy — depth first, left to right, clauses in text order — is not the complete SLD search: a goal that has a refutation can send the interpreter down an infinite branch and never reach it, so completeness belongs to the SLD tree rather than to the language. The cut has no declarative reading; it prunes the tree, so a program containing it is not equivalent to the clauses it contains, and the same holds for assert and retract. Most implementations omit the occurs check, which makes unification unsound and lets X = f(X) succeed on a cyclic term. Negation as failure is not classical negation, is justified only against the completion, and flounders on non-ground negative goals. Clause heads are single atoms, so disjunctive and genuinely existential conclusions cannot be stated at all.