Stream: Coq users

Topic: ✔ Theorem prover vs proof assistant


view this post on Zulip Julin S (Jan 24 2022 at 05:14):

Probably a silly question, but what is the difference between a theorem prover and a proof assistant? Is it that a theorem prover will do more of proof automation or something?

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 07:45):

Somebody will correct me but AFAIK, an interactive theorem prover (such as Coq) seems the same thing. Automated theorem provers are things like SMT solvers, and often they don't let you write proof scripts: they'll just do the proof (or not) and maybe accept hints (theorem statements), but typically support weaker logics...

view this post on Zulip Karl Palmskog (Jan 24 2022 at 08:47):

yeah as Paolo says, "theorem prover" is usually a catchall for both interactive and fully automated systems that claim to verify logical statements (or "equivalently", check fancy types)

view this post on Zulip Paolo Giarrusso (Jan 24 2022 at 09:52):

isn’t “equivalently” just about dependent types, Karl? I recall you also use the HOL family…

view this post on Zulip Karl Palmskog (Jan 24 2022 at 09:56):

indeed the quotation marks in "equivalently" are meant to convey that there are a bunch of caveats, such as that you need dependent types to reduce proof checking to type checking. The HOL family has proof checking for statements that are typed terms, but their proof checkers are not type checkers.

view this post on Zulip Julin S (Jan 25 2022 at 05:46):

Thanks folks.

view this post on Zulip Notification Bot (Jan 25 2022 at 05:46):

Julin S has marked this topic as resolved.


Last updated: Feb 06 2023 at 13:03 UTC