Isabelle is an interactive theorem prover, mostly used as Isabelle/HOL which is based on higer-order logic
Isabelle is a generic interactive prover. The most-used instance is Isabelle/HOL, a theorem prover based on Higher-order logic.
About
Stats
|
created |
8 years, 6 months ago |
|
viewed |
5 times |
|
active |
6 years, 11 months ago |
|
editors |
2 |
Top Answerers
more »
Recent Hot Answers
How did 'Isabelle' (the theorem prover) get its name?How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"?
Naming facts exported from blocks in Isabelle/HOL
When can the coinduction hypothesis be used?
Difference between $\Rightarrow$, $\Longrightarrow$ and $\rightarrow$ in Isabelle/HOL?
more »