4 ms·
Yes. A lot of proof automation is based on SAT/SMT solvers like Z3, which are based on classical logic.
by GregarianChild 2y ago
Yes.
A lot of proof automation is based on SAT/SMT solvers like Z3, which are based on classical logic.
- auggierose 2y agoIt is funny that Z3 was done by the Lean guy. But it probably also explains that Lean basically switched to classical logic.
- hackandthink 2y agoThere ist Jeremy Avigad's influence. He is not the typical type theorist and definitely no constructive zealot. "I have been contributing to the development of the Lean Theorem Prover since its inception. I led the development of the first libraries and documentation.." "Many parts of classical mathematics, however, have not been developed constructively." https://www.andrew.cmu.edu/user/avigad/research.html https://www.andrew.cmu.edu/user/avigad/research.html https://www.andrew.cmu.edu/user/avigad/Teaching/classical.pdf https://www.andrew.cmu.edu/user/avigad/Teaching/classical.pd...
- auggierose 2y agoYes, I know him.