Admin/website/overview.html
author paulson
Fri, 17 Jun 2005 11:35:35 +0200
changeset 16416 6061ae1f90f2
parent 16296 f05c81817ec6
child 16584 991ecdd985d9
permissions -rw-r--r--
grammar fix

<?xml version='1.0' encoding='iso-8859-1' ?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<!-- $Id$ -->
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
    <title>Overview</title>
    <?include file="//include/htmlheader.include.html"?>
</head>

<body class="main">
    <?include file="//include/header.include.html"?>
    <div class="hr"><hr/></div>
    <?include file="//include/navigation.include.html"?>
    <div class="hr"><hr/></div>
    <div id="content">
      <h2>What is Isabelle?</h2> 
      <p>
      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 <em>formal verification</em>, which includes proving
      the correctness of computer hardware or software and proving
      properties of computer languages and protocols.</p>
    
      <p>Compared with similar tools, Isabelle's distinguishing feature is its
      flexibility. Most proof assistants are built around a single formal calculus,
      typically higher-order logic. Isabelle has the capacity to accept a variety
      of formal calculi. The distributed version supports higher-order logic but
      also axiomatic set theory and several other formalisms. See
      <a href="logics.html">logics</a> for more details.</p>

      <p>Isabelle is a joint project between Lawrence C. Paulson
      (University of Cambridge, UK) and Tobias Nipkow (Technical
      University of Munich, Germany).</p>

      <h2>Preview of Isabelle</h2>

        <a href="//media/pg_preview.mov">
            <img class="left" src="//img/isabelle_pg_screenshot_small.png" alt="Sreenshot "
                width="250" height="277" />
        </a>

        <p>Here is a <a href="//media/pg_preview.mov">hyperlinked preview</a> demonstrating
        Isabelle and ProofGeneral, in <a href="http://www.apple.com/quicktime/download/">QuickTime
        format</a>, and also as a <a href="//media/pg_preview.pdf">non-hyperlinked preview</a> in PDF.</p>
        <br clear="all"/>

      <h2>What Isabelle offers</h2>

      <p>Isabelle provides excellent notational support: new notations
      can be introduced, using normal mathematical symbols. Proofs can
      be written in a structured notation based upon traditional proof
      style, or more straightforwardly as sequences of
      commands. Definitions and proofs may include TeX source, from
      which Isabelle can automatically generate typeset documents.</p>

      <p>The main limitation of all such proof systems is that proving
      theorems requires much effort from an expert user. Isabelle
      incorporates some tools to improve the user's productivity by
      automating some parts of the proof process. In particular,
      Isabelle's <em>classical reasoner</em> can perform long chains
      of reasoning steps to prove formulas. The <em>simplifier</em>
      can reason with and about equations. Linear <em>arithmetic</em>
      facts are proved automatically.</p>

      <p>Isabelle comes with a large theory library of formally
      verified mathematics, including elementary number theory (for
      example, Gauss's law of quadratic reciprocity), analysis (basic
      properties of limits, derivatives and integrals), algebra (up to
      Sylow's theorem) and set theory (the relative consistency of the
      Axiom of Choice). Also provided are numerous examples arising
      from research into formal verification.</p>

      <p>With <em>Isar</em>, Isabelle offers a concise proof formulation language
      which enables a user to write proof scripts naturally understandable for
      both humans <em>and</em> computers.</p>
      
      <p>Isabelle is closely integrated with the <a href=
      "http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> user interface, which
      eases the task of writing and maintaining proof scripts.</p>
      <br clear="all" />

      <p>Ample <a href="dist/documentation.html">documentation</a> is available
      about using Isabelle and its inner concepts, including a
      <a href="http://www4.in.tum.de/~nipkow/LNCS2283/">Tutorial</a> published by
      Springer-Verlag.</p>

      <h2>Projects</h2>

      <p>There is an (incomplete) list of past and present <a href=
      "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/projects.html">projects</a>
      undertaken using Isabelle available.</p>

      <h2>License</h2>
          
      <p>Isabelle is distributed free of charge under the open source
      <!--a href="//dist/packages/Isabelle/COPYRIGHT"-->BSD license<!--/a-->. You may use any of our <a
      href="dist/index.html">mirrors</a> for download.</p>
    
    </div>
    <div class="hr"><hr/></div>
    <?include file="//include/footer.include.html"?>
</body>

</html>