Three parent facts form a family chain. Two rules turn that chain into the complete ancestor relation, and EyeProlog derives every pair, says why each holds, and checks its own reasons.
Run it in the playground · Source
Given who is a parent of whom, which people are ancestors of which others?
A parent is an ancestor, and so is a parent of an ancestor. That sentence is the whole program. Nothing in it says how to search; the search follows from the clauses.
parent(pat, jan).
parent(jan, lies).
parent(lies, emma).
Each fact is one sentence: parent(pat, jan) says that Pat is a parent of
Jan. Four generations, three facts.
ancestor(X, Y) :-
parent(X, Y).
ancestor(X, Z) :-
parent(X, Y),
ancestor(Y, Z).
The first clause is the base case: every parent is an ancestor. The second is the recursive case: take one parent step, then ask the same question one generation down. Every recursive call moves one step along a finite chain, so the search ends.
eyeprolog examples/ancestor.pl
ancestor(pat, jan).
ancestor(jan, lies).
ancestor(lies, emma).
ancestor(pat, lies).
ancestor(pat, emma).
ancestor(jan, emma).
Three direct ancestors and three indirect ones. The parent/2 facts are
asked about too, but the output leaves out answers that only repeat a source
fact.
eyeprolog --proof examples/ancestor.pl
step(ancestor(pat, lies),
rule(5),
['X' = pat, 'Z' = lies, 'Y' = jan],
[parent(pat, jan), ancestor(jan, lies)]).
step(ancestor(jan, lies), rule(4), ['X' = jan, 'Y' = lies], [parent(jan, lies)]).
Pat is an ancestor of Lies by the recursive rule (clause 5) with Y = jan: Pat
is Jan’s parent, and Jan is an ancestor of Lies by the base rule (clause 4).
Each conclusion gets exactly one step, and each step names the clause it used.
eyeprolog --proof examples/ancestor.pl > ancestor.why.pl
eyeprolog --check-proof ancestor.why.pl examples/ancestor.pl
condition('C1', resolution, ok, 9).
condition('C4', coverage, ok, 15).
condition('C7', relevance, ok, 15).
verdict(checked).
A separate checker replays all 9 steps against the program without searching. Every claim is covered, every step resolves against the clause it cites, and nothing in the proof is taken on trust.
parent(emma, noor). and predict how many new ancestor pairs appear.--goal 'ancestor(Who, emma)'.Y.Learn more in The Art of EyeProlog, Chapter 4.