3 ms·
Theorem prover seems to misleading. It seems to be an SMT solver, not a competitor to Isabelle, Coq, etc.
by qznc 15y ago
Theorem prover seems to misleading. It seems to be an SMT solver, not a competitor to Isabelle, Coq, etc.
- sanxiyn 15y agoWell, SMT solvers do prove theorems, just not kind of theorems that mathematicians care about. Wikipedia thinks the usage is OK. "Theorem prover may refer to: Automated theorem prover, or Proof assistant, an interactive theorem prover." http://en.wikipedia.org/wiki/Theorem_prover http://en.wikipedia.org/wiki/Theorem_prover