3 ms·
These notions are actually becoming more and more intermixed. You could say today that interactive theorem proving (what is done in a proof assistant) is an ext
by auggierose 9y ago
These notions are actually becoming more and more intermixed. You could say today that interactive theorem proving (what is done in a proof assistant) is an extension of automated theorem proving, as for example the Isabelle proof assistant has very strong support for proving intermediate theorems automatically.
- fizixer 9y agoThanks, I think this is a good example of what I'm looking for. One key ingredient is the presence of a logic inference engine (and not for type inference only, as in Coq, Haskell). - If your system doesn't have a logic inference engine, it's a vanilla proof-assistant (Coq). - If it has one, it's one of two: - a partially-automated theorem prover, (Isabelle) - a fully-automated theorem prover P.S.: Wait a minute. It just occurred to me, is Coq using its Hindley-Milner Type Inference engine as a Logic Inference engine for verifying constructed proofs of theorems and propositions? (is that the killer idea?)