I know that there exist type theory based proof-checker, and I know that there are logic/sequent-calculus based automated theorem provers.

But I haven’t heard of a type-theory based automated theorem prover (nor of a sequent-calculus based proof-checker). Does a type-theory based ATP exist? (And a sequent-calculus based proof-checker?)

If not, why is it that type theory is more fit for proof-checking, and sequent-calculus more fit for proof-finding?

  • $\begingroup$ Several theorem provers have been implemented in Haskell, which has a built-in Hindley-Milner type inference system. $\endgroup$ – Anderson Green Dec 17 '18 at 0:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.