A proof assistant is software used for creating and checking formal proofs; examples include Coq and HOL. Not to be used for requesting assistance on finding proofs.
Stats
created |
2 months ago |
viewed |
3 times |
editors |
0 |
Top Answerers
more »Recent Hot Answers
Why is it so difficult to write complete (computer verifiable) proofs?How do they verify a verifier of formalized proofs?
How do they verify a verifier of formalized proofs?
Function extensionality: does it make a difference? why would one keep it out of the axioms?
Why is it so difficult to write complete (computer verifiable) proofs?
more »
Related Tags
lo.logic × 7
coq × 3
proof-theory × 3
type-theory × 2
soft-question × 2
formalisation × 2
more related tags