Theorem prover seems to misleading. It seems to be an SMT solver, not a competit... | Hacker News

Hacker News new | past | comments | ask | show | jobs | submit

login

qznc on April 13, 2012 | parent | context | favorite | on: Rise4fun - from Microsoft Research

Theorem prover seems to misleading. It seems to be an SMT solver, not a competitor to Isabelle, Coq, etc.

sanxiyn on April 13, 2012 [–]

Well, 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

Consider applying for YC's W25 batch! Applications are open till Nov 12.
Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact