From Newsgroup: comp.lang.prolog
Dear All,
Lets posit this Autum Challenge 2025.
The idea is to forget about Robert St|nrks
proof framework, although impressive,
and it can possibly proof:
a + (b + c) = (a + b) + c
In the natural numbers. Why not try
an entropy based interative deepening,
and simply find a proof justification
for the above in a more undisciplined manner:
Canonical for Automated Theorem Proving in Lean
https://arxiv.org/abs/2504.06239
Unfortunately the above seems to be a Rust
program. Can we implement it in Prolog itself?
Disclaimer: Canonical doesn't meen minimal DFA ,
just in case Julio Di Egidio thinks otherwise.
Bye
--- Synchronet 3.21a-Linux NewsLink 1.2