Our website is made possible by displaying online advertisements to our visitors.
Please consider supporting us by disabling your ad blocker.
Isabelle (proof assistant)
&sq=crain_ford&lang=en&file=File:Isabelle_jedit.png) Isabelle–jEdit running on macOS | |
| Original author(s) | Lawrence Paulson |
|---|---|
| Developer(s) | University of Cambridge Technical University of Munich, et al. |
| Initial release | 1986[1] |
| Stable release | Isabelle2024
/ May 2024 |
| Written in | Standard ML, Scala |
| Operating system | Linux, Windows, macOS |
| Type | Mathematics |
| License | BSD |
| Website | isabelle |
The Isabelle[a] automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As a Logic for Computable Functions (LCF) style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring, yet supporting, explicit proof objects.
Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories and implementations for code-generating, documenting, and specific support for a variety of formal methods. It can be seen as an integrated development environment (IDE) for formal methods. In recent years, a substantial number of theories and system extensions have been collected in the Isabelle Archive of Formal Proofs (Isabelle AFP)[2]
Isabelle was named by Lawrence Paulson after Gérard Huet's daughter.[3]
The Isabelle theorem prover is free software, released under the revised BSD license.
- ^ Paulson, L. C. (1986). "Natural deduction as higher-order resolution". The Journal of Logic Programming. 3 (3): 237–258. arXiv:cs/9301104. doi:10.1016/0743-1066(86)90015-4. S2CID 27085090.
- ^ Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René. "Archive of Formal Proofs". Retrieved 1 May 2021.
- ^ Gordon, Mike (1994-11-16). "1.2 History". Isabelle and HOL. Cambridge AR Research (The Automated Reasoning Group). Archived from the original on 2017-03-05. Retrieved 2016-04-28.
Cite error: There are <ref group=lower-alpha> tags or {{efn}} templates on this page, but the references will not show without a {{reflist|group=lower-alpha}} template or {{notelist}} template (see the help page).
Previous Page Next Page
