Isabelle is a generic proof assistant.
It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. The main application is the formalization of mathematical proofs and in particular formal verification, which includes proving the correctness of computer hardware or software and proving properties of computer languages and protocols.
The most widespread instance of Isabelle nowadays is Isabelle/HOL, which provides a higher-order logic theorem proving environment that is ready to use for big applications.
Isabelle/HOL includes powerful specification tools, e.g. for (co)datatypes, (co)inductive definitions and recursive functions with complex pattern matching.
Proofs are conducted in the structured proof language Isar, allowing for proof text naturally understandable for both humans and computers.
For proofs, Isabelle incorporates some tools to improve the user’s productivity. In particular, Isabelle’s classical reasoner can perform long chains of reasoning steps to prove formulas. The simplifier can reason with and about equations. Linear arithmetic facts are proved automatically, various algebraic decision procedures are provided. External first-order provers can be invoked through sledgehammer.
Isabelle may serve as a generic framework for rapid prototyping of deductive systems. These are formulated within Isabelle’s logical framework Isabelle/Pure, which is suitable for a variety of formal calculi (e.g. axiomatic set theory).
Isabelle allows proofs to be written in two different styles, the procedural and the declarative.
This is free and open source software.
Website: isabelle.in.tum.de
Support: Documentation
Developer: University of Cambridge, Technische Universitaet Muenchen, and contributors
License: BSD-style
Isabelle is written in Standard ML and Scala. Learn Standard ML with our recommended free books and free tutorials. Learn Scala with our recommended free books and free tutorials.
Related Software
| Proof Assistants | |
|---|---|
| Rocq Prover | Formal proof management system |
| Isabelle | Generic proof assistant; express mathematical formulas in a formal language |
| Lean | Programming language and theorem prover |
| Agda | Interactive system for writing and checking proofs |
| F* | Functional language for verified programs with dependent refinement types |
| HOL4 | Interactive higher-order logic environment for rigorous theorem development |
| Aya | Dependently typed language for formalisation and certified programming |
| Lambdapi | Logical framework for defining and checking expressive type systems |
| HOL Light | Lightweight higher-order logic system with a small trusted kernel |
| PVS | Specification and verification suite for analysing complex systems |
| LISA | Scala-based platform for formal mathematics and automated reasoning |
Read our verdict in the software roundup.
 Explore our carefully curated directory of recommended free and open source software, covering every major software category.The directory forms part of our extensive collection of articles for Linux enthusiasts. It includes hundreds of detailed reviews, together with free and open source alternatives to proprietary software from companies such as Google, Microsoft, Apple, Adobe, IBM, Cisco, Oracle, and Autodesk. LinuxLinks also covers interesting projects worth exploring, Linux-compatible hardware, free programming books and tutorials, and much more. Know a useful free and open source Linux application that we haven’t covered? Tell us about it using our submission form. |
Please read our Comment Policy before commenting.