Julin S (Jan 24 2022 at 05:14): 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?
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...
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)
Paolo Giarrusso (Jan 24 2022 at 09:52):isn’t “equivalently” just about dependent types, Karl? I recall you also use the HOL family…
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.
Julin S (Jan 25 2022 at 05:46):Thanks folks.
Notification Bot (Jan 25 2022 at 05:46):Julin S has marked this topic as resolved.
Last updated: Apr 19 2024 at 14:02 UTC