Ten thousand steps of reasoning, every one written down and checked.
deep-taxonomy-10000.pl · output · proof · check · try it in the playground
A taxonomy is a tree of categories: a robin is a bird, a bird is an animal, and so on. Here the tree is ten thousand levels deep, and at every level it also splits into two side branches that go nowhere.
We know one thing: an individual, ind, is in the top category n0.
Is ind in category n10000, at the very bottom? And can the computer
show all ten thousand steps — and have them checked?
This is the deep-taxonomy benchmark, a standard stress test for reasoners. The collection has it at four depths, and this is the largest:
| Example | Levels | Proof steps |
|---|---|---|
| deep-taxonomy-10 | 10 | 11 |
| deep-taxonomy-100 | 100 | 101 |
| deep-taxonomy-1000 | 1000 | 1001 |
| deep-taxonomy-10000 | 10000 | 10001 |
Same shape each time; only the length of the chain changes.
One fact, then three rules per level — 30,000 rules in all:
type(ind, n0).
type(X, n1) :- type(X, n0).
type(X, i1) :- type(X, n0).
type(X, j1) :- type(X, n0).
type(X, n2) :- type(X, n1).
% … and so on, down to
type(X, n10000) :- type(X, n9999).
type(X, i10000) :- type(X, n9999).
type(X, j10000) :- type(X, n9999).
true :+ type(X, n10000).
Read type(X, n2) :- type(X, n1) as anything in n1 is also in n2. The
i and j rules are the dead-end side branches. The last line asks the
question.
type(ind, n10000).
One answer: yes.
Eyedia works backward from the question (:- rules are explored only when
a question needs them): to be in n10000, be in n9999; to be in n9999,
be in n9998; … all the way up to the fact we gave. The search is an
explicit machine inside Eyedia, so ten thousand levels deep is no problem.
The proof is a chain of 10,001 steps:
ind is in n0 — a fact we gave (fact 1).ind is in n1 — rule 2.ind is in n2 — rule 5.ind is in n10000 — rule 29999.Each step names the exact program line it used. The 20,000 side-branch rules never appear: they do not help answer the question.
A separate checker read all 10,001 steps against the program and confirmed that:
Verdict: checked. All 10,001 steps verified, and nothing taken on trust.
The source is about 1 MB and its proof about 1.3 MB: a proof records every step it claims.
node bin/eyedia.js examples/deep-taxonomy-10000.pl # the answer
node bin/eyedia.js --stats examples/deep-taxonomy-10000.pl # and its cost
--stats reports "inferences":10001 — one step per level, plus the fact.
Or open it in the playground.
Change the last line to true :+ type(X, j5000). and run with --stats
again: the answer is type(ind, j5000), a side branch halfway down,
reached in 5001 steps.
Going from ten levels to ten thousand changes the cost, not the kind of answer. Time, proof size and checking all grow in step with the depth, so a ten-thousand-step argument is just as followable — and just as checkable — as a ten-step one.