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

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.