Isabelle

Introduction

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. Isabelle is developed at University of Cambridge (Larry Paulson), Technische Universität München (Tobias Nipkow) and Université Paris-Sud (Makarius Wenzel). See the Isabelle overview for a brief introduction.

Usage

Compute Systems Invocation Version(s)
Red Hat Linux (64-bit) % /util/bin/isabelle NAME [ARGS ...] 2011-1 (default)

Notes

  1. You may invoke Isabelle with a variety of interface wrappers. We recommend: 
    
% isabelle jedit
  2. If you invoke Isabelle with the Emacs interface wrapper, exit with Ctrl-x c

People

  1. Bharat Jayaraman, instructor.

References

  1. http://en.wikipedia.org/wiki/Isabelle_%28proof_assistant%29
  2. http://isabelle.in.tum.de/index.html
  3. http://isabelle.in.tum.de/overview.html
  4. https://isabelle.in.tum.de/community/Projects