A thousand-step chain of reasoning, every step written down and checked.
deep-taxonomy-1000.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 a 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 n1000, at the very bottom? And can the computer
show every one of the thousand steps?
This is the deep-taxonomy benchmark, a standard stress test for reasoners. The collection has it at four depths:
| 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 — 3000 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, n1000) :- type(X, n999).
type(X, i1000) :- type(X, n999).
type(X, j1000) :- type(X, n999).
true :+ type(X, n1000).
Read type(X, n2) :- type(X, n1) as anything in n1 is also in n2. The
i and j rules are the side branches. The last line asks the question.
type(ind, n1000).
One answer: yes, ind is in n1000.
Eyedia works backward from the question (:- rules are explored when a
question needs them): to be in n1000, be in n999; to be in n999, be in
n998; … all the way up to the fact we gave.
The proof is a chain of 1001 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 n1000 — rule 2999.Each step names the exact program line it used. The side branches never appear: they do not help answer the question.
A separate checker read all 1001 steps against the program and confirmed that:
Verdict: checked. All 1001 steps verified, and nothing taken on trust.
The source is about 96 KB and its proof about 126 KB: a proof records every step it claims.
node bin/eyedia.js examples/deep-taxonomy-1000.pl # the answer
node bin/eyedia.js --stats examples/deep-taxonomy-1000.pl # and its cost
--stats reports "inferences":1001 — one step per level, plus the fact.
Or open it in the playground.
Change the last line to true :+ type(X, i500). and run with --stats
again: the answer is type(ind, i500), reached in 501 steps.
Long reasoning does not have to be opaque. Time, proof size and checking grow in step with the depth, so a chain a thousand steps long is just as followable — and just as checkable — as one with ten.