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.
| Popular series | |
|---|---|
 | The largest compilation of the best free and open source software in the universe. Each article is supplied with a legendary ratings chart helping you to make informed decisions. |
 | Hundreds of in-depth reviews offering our unbiased and expert opinion on software. We offer helpful and impartial information. |
 | The Big List of Active Linux Distros is a large compilation of actively developed Linux distributions. |
 | Replace proprietary software with open source alternatives: Google, Microsoft, Apple, Adobe, IBM, Autodesk, Oracle, Atlassian, Corel, Cisco, Intuit, and SAS. |
 | Awesome Free Linux Games Tools showcases a series of tools that making gaming on Linux a more pleasurable experience. This is a new series. |
 | Machine Learning explores practical applications of machine learning and deep learning from a Linux perspective. We've written reviews of more than 40 self-hosted apps. All are free and open source. |
 | New to Linux? Read our Linux for Starters series. We start right at the basics and teach you everything you need to know to get started with Linux. |
 | Alternatives to popular CLI tools showcases essential tools that are modern replacements for core Linux utilities. |
 | Essential Linux system tools focuses on small, indispensable utilities, useful for system administrators as well as regular users. |
 | Linux utilities to maximise your productivity. Small, indispensable tools, useful for anyone running a Linux machine. |
 | Surveys popular streaming services from a Linux perspective: Amazon Music Unlimited, Myuzi, Spotify, Deezer, Tidal. |
 | Saving Money with Linux looks at how you can reduce your energy bills running Linux. |
 | Home computers became commonplace in the 1980s. Emulate home computers including the Commodore 64, Amiga, Atari ST, ZX81, Amstrad CPC, and ZX Spectrum. |
 | Now and Then examines how promising open source software fared over the years. It can be a bumpy ride. |
 | Linux at Home looks at a range of home activities where Linux can play its part, making the most of our time at home, keeping active and engaged. |
 | Linux Candy reveals the lighter side of Linux. Have some fun and escape from the daily drudgery. |
 | Getting Started with Docker helps you master Docker, a set of platform as a service products that delivers software in packages called containers. |
 | Best Free Android Apps. We showcase free Android apps that are definitely worth downloading. There's a strict eligibility criteria for inclusion in this series. |
 | These best free books accelerate your learning of every programming language. Learn a new language today! |
 | These free tutorials offer the perfect tonic to our free programming books series. |
 | Linux Around The World showcases usergroups that are relevant to Linux enthusiasts. Great ways to meet up with fellow enthusiasts. |
 | Stars and Stripes is an occasional series looking at the impact of Linux in the USA. |