The largest deep-taxonomy example and a deliberate stress case. The program is a 300,000-rule chain, its proof is about 12 MB, and the checker replays 100,002 steps. Smaller siblings: 10, 100, 1000, 10000.
Run it in the playground · Source
ind is in n0, each of 100,000 levels lifts it one class higher, and
n100000 implies a2. Is ind in a2?
The logic is the same as at depth 10. The test is whether parsing, solving, proof writing, and proof checking all scale linearly.
a(ind, n0).
a(X, a2) :- a(X, n100000).
a(X, n1) :- a(X, n0).
a(X, i1) :- a(X, n0).
a(X, j1) :- a(X, n0).
Unlike its smaller siblings, this file has no holds_result/2 rule and no
discontiguous directive, so its clause numbers start one earlier: the top
rule is clause 2, not 4.
eyeprolog examples/deep-taxonomy-100000.pl
a(ind, a2).
--stats reports a maximum depth of 100001: one level per class.
step(a(ind, a2), rule(2), ['X' = ind], [a(ind, n100000)]).
step(a(ind, n100000), rule(300000), ['X' = ind], [a(ind, n99999)]).
step(a(ind, n1), rule(3), ['X' = ind], [a(ind, n0)]).
The first step cites the top rule, the second cites clause 300,000 (the
program’s last n rule), and step 100,001 reaches the bottom of the chain.
Only the n rules appear: the 200,000 side-label rules are never touched.
condition('C1', resolution, ok, 100002).
condition('C2', well_founded, ok, 100002).
condition('C4', coverage, ok, 100002).
condition('C7', relevance, ok, 100003).
steps(100002).
trusted(0).
verdict(checked).
Every one of the 100,002 steps is replayed against the clause it cites. At this scale an independent check is the only practical way to trust a proof: no person will read it.
--goal 'a(ind, n50000)' and confirm the proof stops halfway.npm test and find where this example’s proof is checked.Learn more in The Art of EyeProlog, Chapters 11 and 40.