Yes! The prover is really any function with two semantic guarantees:
If (eval exp) returns #f, so does (prove exp).
(prove exp) does not do unbounded computation, and always returns either #t or #f.
The prover does not need to be a good prover, but ideally it would be self-aware, looking for instances of prove in the expression to try to find fixed points. Note that when writing a bot, one can internally define and use their own theorem prover if they wish—and in a more barebones competition the competitor would be required to.
can the
provefunction make use of facts like’(prove X)?Yes! The prover is really any function with two semantic guarantees:
If
(eval exp)returns#f, so does(prove exp).(prove exp)does not do unbounded computation, and always returns either#tor#f.The prover does not need to be a good prover, but ideally it would be self-aware, looking for instances of
provein the expression to try to find fixed points. Note that when writing a bot, one can internally define and use their own theorem prover if they wish—and in a more barebones competition the competitor would be required to.