Logic Programming

Origin. Kowalski, Colmerauer (1970s). Computation as deduction. Horn clauses. Prolog. Foundation for declarative programming.

Models. Programs as logical theories. SLD resolution. Minimal Herbrand model. Negation as failure. Unification-based.

Formalism.

Horn clause: H :- B₁, ..., Bₙ. Head H true if body B₁ ∧ ... ∧ Bₙ true.

Fact: H. Clause with empty body. H always true.

Query: ?- G₁, ..., Gₘ. Find substitution making goals true.

SLD resolution: Select goal Gᵢ. Unify with head H of clause. Replace Gᵢ with body. Apply substitution.

Unification: Find σ with σ(t₁) = σ(t₂). Most general unifier. Occurs check.

Minimal model: T_P operator: T_P(I) = {H : (H :- B) ∈ P, I ⊨ B} Least fixed point = minimal model.

Negation as failure: not G succeeds if G finitely fails. Closed world assumption. SLDNF resolution.

Cut: !: commit to choices. Control backtracking. Affects logical reading.

Definite clause grammars: DCG: grammar as logic program. Parsing as theorem proving.

Symbols.

Symbol	Unicode	Name	Meaning
:-	—	If	Clause arrow
?-	—	Query	Goal
,	—	And	Conjunction
not	—	NAF	Negation as failure

Metatheory. Sound: answers are logical consequences. Complete for Horn: all consequences found. Negation complicates.

Applies to. Prolog. Databases (Datalog). AI planning. Expert systems. Constraint solving.

Limitations. Order-dependence. Cut affects meaning. Non-termination. Negation subtle.