Isabelle – generic proof assistant

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 C with our recommended free books and free tutorials. Learn Scala with our recommended free books and free tutorials.

Return to Proof Assistants Home Page


Popular series
Guide to LinuxNew 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.
Free and Open Source SoftwareThe 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.
ReviewsHundreds of in-depth reviews offering our unbiased and expert opinion on software. We offer helpful and impartial information.
Alternatives to Proprietary SoftwareReplace proprietary software with open source alternatives: Google, Microsoft, Apple, Adobe, IBM, Autodesk, Oracle, Atlassian, Corel, Cisco, Intuit, and SAS.
Linux Around The WorldLinux Around The World showcases events and usergroups that are relevant to Linux enthusiasts.
AudioSurveys popular streaming services from a Linux perspective: Amazon Music Unlimited, Myuzi, Spotify, Deezer, Tidal.
Saving Money with LinuxSaving Money with Linux looks at how you can reduce your energy bills running Linux.
System ToolsEssential Linux system tools focuses on small, indispensable utilities, useful for system administrators as well as regular users.
ProductivityLinux utilities to maximise your productivity. Small, indispensable tools, useful for anyone running a Linux machine.
Home ComputersHome computers became commonplace in the 1980s. Emulate home computers including the Commodore 64, Amiga, Atari ST, ZX81, Amstrad CPC, and ZX Spectrum.
Now and ThenNow and Then examines how promising open source software fared over the years. It can be a bumpy ride.
Linux at HomeLinux 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 CandyLinux Candy reveals the lighter side of Linux. Have some fun and escape from the daily drudgery.
DockerGetting Started with Docker helps you master Docker, a set of platform as a service products that delivers software in packages called containers.
Android AppsBest Free Android Apps. We showcase free Android apps that are definitely worth downloading. There's a strict eligibility criteria for inclusion in this series.
Programming BooksThese best free books accelerate your learning of every programming language. Learn a new language today!
Programming TutorialsThese free tutorials offer the perfect tonic to our free programming books series.
Stars and StripesStars and Stripes is an occasional series looking at the impact of Linux in the USA.
Share this article

Share your Thoughts

This site uses Akismet to reduce spam. Learn how your comment data is processed.