My Reasoning Engine Proved 114 Is Prime: A Negation Bug Story
An open-source reasoning engine's negation bug proved that 114 is prime; a race condition in forward chaining and its fix via stratification are explained.
zelph is an open-source C++ reasoning engine that represents everything — facts, rules, predicates, even numbers — as nodes in a single graph. Numbers are linked lists of digit nodes, and arithmetic operations like addition, multiplication and division are ordinary forward-chaining rules that rewrite the graph rather than built-in code. To showcase this, the author tried to implement a textbook primality test using negation-as-failure: a number is prime if no divisor fact exists for it.
The logically correct rule failed twice as a program. The first bug was trivial: a bare numeric literal parsed as an atom rather than a number, so no arithmetic rule could ever produce a divisor fact, making the negation vacuously true and every number 'prime.' The second, more interesting bug was a race condition inside single-threaded logic: because the engine iterates rules from an unordered hash set, the negation was sometimes evaluated before the corresponding positive fact had been derived. Since forward chaining is monotonic — facts are never retracted — a wrong conclusion, once asserted, became permanent, producing results that depended unpredictably on rule definition order.
The fix was to actually implement stratified evaluation, a technique known since 1980s Datalog theory but not enforced in the engine's code: run all purely positive rules to a fixpoint first, then evaluate negation-containing rules against that saturated fact base, alternating the two phases until nothing new is derived. The same monotonicity that caused the bug also justifies the fix — new facts can only make a negation fail, never newly succeed, so a negation that holds after positive quiescence is final.
After the fix, the engine correctly executes the textbook primality rule using arbitrary-precision arithmetic built entirely from graph-rewriting rules. The standard library also includes a negation-free alternative that proves primality via a positive fold, which runs faster on composite numbers by halting at the smallest divisor. The author's broader takeaways: negation-as-failure in a forward chainer is fundamentally a scheduling problem, order-dependent bugs should be distilled into minimal regression tests, and documenting semantics the code doesn't actually enforce is a bug report written in advance.