eyeprolog

Deep taxonomy, depth 10

Does one individual, climbing ten levels of a class hierarchy, reach the top?

The deep-taxonomy benchmark is a long chain of subclass rules. This is its smallest version: ten levels, small enough to read the whole proof. Its siblings run the same chain at depths 100, 1000, 10000, and 100000.

Run it in the playground · Source

The question

An individual ind belongs to class n0. Every member of n0 is also a member of n1, every member of n1 of n2, and so on up to n10; every member of n10 belongs to a2. Is ind in a2?

The benchmark comes from the Semantic Web, where such chains are written as N3 rules; here each rule is one Prolog clause.

The facts and rules

a(ind, n0).

a(X, a2) :- a(X, n10).

a(X, n1) :- a(X, n0).
a(X, i1) :- a(X, n0).
a(X, j1) :- a(X, n0).
a(X, n2) :- a(X, n1).
a(X, i2) :- a(X, n1).
a(X, j2) :- a(X, n1).

a(X, C) reads “X is a member of class C”. Each level has three rules: one climbs to the next n class, and two add side labels i and j that lead nowhere. The side labels are there to tempt a reasoner into extra work.

The answer

eyeprolog examples/deep-taxonomy-10.pl

a(ind, a2).

Yes: ind reaches the top class.

The reason

eyeprolog --proof examples/deep-taxonomy-10.pl

step(a(ind, a2), rule(4), ['X' = ind], [a(ind, n10)]).
step(a(ind, n10), rule(32), ['X' = ind], [a(ind, n9)]).
step(a(ind, n9), rule(29), ['X' = ind], [a(ind, n8)]).

At this depth the whole proof fits on a slide: 12 steps, from a2 down through n10, n9, … to the fact a(ind, n0). No i or j label appears. EyeProlog works backwards from the question, so it never derives the side labels at all.

The check

condition('C1', resolution, ok, 12).
condition('C4', coverage, ok, 12).
condition('C7', relevance, ok, 13).
steps(12).
trusted(0).
verdict(checked).

The checker replays all 12 steps against the cited clauses. Every step is needed for the claim, and nothing is taken on trust.

Try it

Ask for every class ind belongs to: --goal 'a(ind, X)'. There are 31 answers: n1–n10, i1–i10, j1–j10, and a2.
Ask --goal 'a(ind, j10)' and compare its proof with the one above.
Save the proof, delete the step for a(ind, n5), and run --check-proof on the result. Which conditions fail, and why does a gap in the middle of a chain break more than one link?

Learn more in The Art of EyeProlog, Chapters 4 and 11.

This site is open source. Improve this page.