3 ms·
There exists the software Coq which is a theorem prover. https://en.wikipedia.org/wiki/Coq https://en.wikipedia.org/wiki/Coq
by acd 7y ago
There exists the software Coq which is a theorem prover.
https://en.wikipedia.org/wiki/Coq https://en.wikipedia.org/wiki/Coq
- frabert 7y agoCorrection: it is a proof assistant, not a theorem prover. Z3 (also from De Moura) is a theorem prover. EDIT: Main difference between the two is that with a proof assistant, you write a proof and the assistant checks its correctness, while a prover provides you with a proof of a proposition's correctness (or of its lack thereof).