Facts, rules, queries, and the closed-world assumption

◈ 5 cards

Read a clause declaratively, write facts and head :- body rules, pose a query, and understand why Prolog treats unprovable as false (negation-as-failure).

Prolog is logic you can run

Python is our runtime, but the COMP 456 exam (Q3) and three of the four assignments are written in Prolog. Prolog is declarative: you state what is true, and the interpreter searches for how to prove a goal. A Prolog program is just a set of Horn clauses (Chapter 14), and running a query is resolution-based theorem proving driven by unification (the algorithm from M1).

There are exactly three clause forms, and they map onto the Horn-clause theory one-for-one:

A fact — an unconditional truth. parent(tom, bob). ("tom is a parent of bob").
A rule — head :- body, read "head is true if body is true". The :- is ← ("if"), and the comma in the body is conjunction (∧).
A query (goal) — what you ask at the ?- prompt. The interpreter tries to prove it.

The case convention (the #1 student slip)

In this textbook's notation and in Prolog, lowercase = constant (a specific named object: tom, bob) and an initial uppercase letter = variable (stands for any object: X, Person). Students reverse this constantly — guard against it.

Worked example — a family tree

Facts about who is a parent of whom, then a rule defining grandparent in terms of two parent steps:

parent(tom, bob).
parent(bob, ann).
parent(bob, pat).

grandparent(X, Y) :- parent(X, Z), parent(Z, Y).

Read the rule declaratively: "X is a grandparent of Y if X is a parent of some Z and that Z is a parent of Y." The shared variable Z is the bridge — unification must bind Z consistently in both parent goals. Now ask:

?- grandparent(tom, Who).
Who = ann ;
Who = pat.

The interpreter unifies grandparent(tom, Who) with the rule head (binding X = tom, Y = Who), then proves the body left to right: parent(tom, Z) succeeds with Z = bob, then parent(bob, Who) succeeds with Who = ann. Typing ; asks for the next solution; backtracking re-tries parent(bob, Who) and finds Who = pat.

The closed-world assumption

Prolog assumes its database is complete: anything it cannot prove is taken to be false. This closed-world assumption (CWA) is what lets Prolog implement negation-as-failure with \+: \+ parent(tom, sue) succeeds precisely because Prolog fails to prove parent(tom, sue). The catch (and a favourite exam trap): unprovable means "false" even when the truth is merely unknown — Prolog cannot tell a false fact from a missing one.

Reading down is resolution (a goal is replaced by the body of the rule whose head it unified with); reading across the two leaves is <em>backtracking</em>. Typing <code>;</code> at the first answer discards the binding Who = ann, returns to the last choice point — the two facts about bob — and takes the next one.

Only an uppercase-initial term can bind. Rows 3 and 4 fail for the same reason — a constant must match <em>exactly</em> — which is why <code>parent(x, bob)</code> (lowercase x) is a different query from <code>parent(X, bob)</code>.