Isabelle (proof assistant)
Higher-order logic (HOL) automated theorem prover / From Wikipedia, the free encyclopedia
Dear Wikiwand AI, let's keep it short by simply answering these key questions:
Can you list the top facts and stats about Isabelle theorem prover?
Summarize this article for a 10 year old
The Isabelle[lower-alpha 1] automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an 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.
Original author(s) | Lawrence Paulson |
---|---|
Developer(s) | University of Cambridge and Technical University of Munich et al. |
Initial release | 1986[1] |
Stable release | Isabelle2024
/ May 2024; 2 months ago (2024-05) |
Written in | Standard ML and Scala |
Operating system | Linux, Windows, macOS |
Type | Mathematics |
License | BSD license |
Website | isabelle |
Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of formal methods. It can be seen as an 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.