My reasoning engine proved that 114 is prime — a debugging story about negation

A developer building the open-source reasoning engine zelph discovered a bug where the engine incorrectly proved that 114 is prime due to a race condition in single-threaded logic. The bug occurred because negation-as-failure was evaluated before all relevant facts were derived, and the engine's monotonic nature prevented retraction of wrong conclusions. The fix ensures negation is evaluated only after positive inference reaches quiescence.

zelph 114 testprime 114 114 isprime 114 ⇐ { ¬ 114 hasdivisor D 114 testprime 114 } 114 is 2 · 3 · 19. My engine was very confident it's prime. Even better: it printed a proof . Quick context: I build zelph https://github.com/acrion/zelph , an open-source reasoning engine C++ where everything is one graph — facts, rules, predicates, even numbers. There is no arithmetic code in the engine core: numbers are linked lists of digit nodes, and addition, comparison, multiplication and division are ordinary inference rules that rewrite the graph how that works https://acrion.github.io/zelph/arithmetic/ . As a showcase, I wanted a primality test written the way a textbook states it: N is prime if no candidate divides it. In zelph syntax: js N testprime N, ¬ N hasdivisor D = N isprime N ¬ is negation-as-failure: the condition succeeds if no matching fact exists. Other rules enumerate divisor candidates and assert N mod D facts, which the division module answers. The rule looks correct. It even is correct — as a formula. As a program, it was broken twice. In zelph, 114 without a prefix parses as an atom — a node whose name is "114" — not as a digit list. No arithmetic rule can divide an atom, so no hasdivisor fact could ever exist, so the negation was trivially true, so everything was prime. The classic "your test tests nothing" bug, in logic form. Fix: number literals are written &114 . Moving on — because bug 2 is the one worth a blog post. Even with real numbers, the rule kept deriving isprime for composite numbers — sometimes , depending on the order in which rules had been defined. When a bug depends on ordering, I stop debugging the big system and distill. This is the entire bug class in four lines: js A trigger A = A step1 A A step1 A = A step2 A A trigger A, ¬ A step2 A = A racewin A x trigger x step2 is always derivable from trigger . So racewin should never fire. The old engine: x step1 x ⇐ x trigger x x racewin x ⇐ { ¬ x step2 x x trigger x } x step2 x ⇐ x step1 x There it is, in the output order: the negation was evaluated while the answer was still being computed . At that moment x step2 x didn't exist yet , so ¬ ... succeeded, so racewin was derived. And here's the trap that makes this fatal rather than transient: A forward chainer is monotonic. Facts are only ever added, never retracted. When step2 arrived one inference step later, it was too late — the wrong conclusion was already a fact, with a proof attached, and nothing in the engine's universe could take it back. For the primality test this meant: isprime 42 raced against dozens of mod computations cascading through many fixpoint iterations. Whoever finished first won. A variation of the probe — same shape, one extra indirection — produced the correct result on my machine. Why? Because the engine iterates its rules from an unordered hash set, and the hash order happened to schedule the fact-producing rule before the negation rule. I've debugged race conditions between threads before. A race condition inside single-threaded logic , decided by unordered set iteration order, was new to me. The theory has been known since the 1980s stratified Datalog . My own documentation even claimed zelph had these semantics. The engine just... didn't implement them. Ouch. The fix: ¬ at any nesting depth form a The soundness argument is one sentence, and I find it satisfying that the villain of this story is also the hero: monotonicity caused the bug no retraction and also fixes it — new facts can make a negation fail , but never make it newly succeed . So a negation that succeeds after positive quiescence is final. The four-line repro and its friends are now permanent regression tests in the suite. python zelph .import arithmetic zelph .import primes-naf zelph &113 testprime &113 = X &113 testprime &113 = prime ⇐ { &113 isprime &113 ...} zelph &42 testprime &42 = X &42 testprime &42 = composite ⇐ { &42 hasdivisor &2 ...} The textbook rule, executable as written — with the entire arithmetic underneath comparison, subtraction, multiplication, Euclidean division with remainder running as forward-chaining graph rewriting, arbitrary precision included. One more thing I find mildly beautiful: the standard library also ships a negation-free twin primes.zph . It proves primality via a positive fold — "no divisor up to D" grows one verified candidate at a time — and the fold doubles as a scheduler : for composite N, the search halts at the smallest divisor. On composites it's roughly 3–4× faster than the eager NAF version; on primes they tie, because both must pay for the full scan up to √N. Same mathematics, two proof strategies — and the proof strategy is the execution strategy. ¬ against in-flight state, you have a race — you just haven't lost it yet.Release notes for v0.9.8: https://github.com/acrion/zelph/releases/tag/v0.9.8 https://github.com/acrion/zelph/releases/tag/v0.9.8 Try it: brew tap acrion/zelph && brew install zelph · choco install zelph · AUR: zelph A question for people who've built or used forward-chaining systems Datalog engines, rule engines, CEP systems : how does yours schedule negation? Static stratification analysis at compile time, runtime deferral like this, well-founded semantics, something else entirely? I chose runtime deferral because zelph's rules quantify over predicates predicates are graph nodes , which makes static predicate-level stratification too coarse — but I'd genuinely like to hear other approaches.