Admin/website/overview.html
author haftmann
Mon, 06 Jun 2005 14:12:07 +0200
changeset 16301 f9f2e1643593
parent 16296 f05c81817ec6
child 16416 6061ae1f90f2
permissions -rw-r--r--
migrated scripts to new webiste
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
     1
<?xml version='1.0' encoding='iso-8859-1' ?>
e634d33deb86 added new website
haftmann
parents:
diff changeset
     2
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
     3
<!-- $Id$ -->
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
     4
<html xmlns="http://www.w3.org/1999/xhtml">
e634d33deb86 added new website
haftmann
parents:
diff changeset
     5
e634d33deb86 added new website
haftmann
parents:
diff changeset
     6
<head>
e634d33deb86 added new website
haftmann
parents:
diff changeset
     7
    <title>Overview</title>
e634d33deb86 added new website
haftmann
parents:
diff changeset
     8
    <?include file="//include/htmlheader.include.html"?>
e634d33deb86 added new website
haftmann
parents:
diff changeset
     9
</head>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    10
e634d33deb86 added new website
haftmann
parents:
diff changeset
    11
<body class="main">
e634d33deb86 added new website
haftmann
parents:
diff changeset
    12
    <?include file="//include/header.include.html"?>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    13
    <div class="hr"><hr/></div>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    14
    <?include file="//include/navigation.include.html"?>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    15
    <div class="hr"><hr/></div>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    16
    <div id="content">
e634d33deb86 added new website
haftmann
parents:
diff changeset
    17
      <h2>What is Isabelle?</h2> 
e634d33deb86 added new website
haftmann
parents:
diff changeset
    18
      <p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    19
      Isabelle is a generic proof assistant. It allows mathematical
e634d33deb86 added new website
haftmann
parents:
diff changeset
    20
      formulas to be expressed in a formal language and provides tools
e634d33deb86 added new website
haftmann
parents:
diff changeset
    21
      for proving those formulas in a logical calculus.  The main
e634d33deb86 added new website
haftmann
parents:
diff changeset
    22
      application is the formalization of mathematical proofs and in
e634d33deb86 added new website
haftmann
parents:
diff changeset
    23
      particular <em>formal verification</em>, which includes proving
e634d33deb86 added new website
haftmann
parents:
diff changeset
    24
      the correctness of computer hardware or software and proving
e634d33deb86 added new website
haftmann
parents:
diff changeset
    25
      properties of computer languages and protocols.</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    26
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    27
      <p>Compared with similar tools, Isabelle's distinguishing feature is its
e634d33deb86 added new website
haftmann
parents:
diff changeset
    28
      flexibility. Most proof assistants are built around a single formal calculus,
e634d33deb86 added new website
haftmann
parents:
diff changeset
    29
      typically higher-order logic. Isabelle has the capacity to accept a variety
e634d33deb86 added new website
haftmann
parents:
diff changeset
    30
      of formal calculi. The distributed version supports higher-order logic but
e634d33deb86 added new website
haftmann
parents:
diff changeset
    31
      also axiomatic set theory and several other formalisms. See
e634d33deb86 added new website
haftmann
parents:
diff changeset
    32
      <a href="logics.html">logics</a> for more details.</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    33
e634d33deb86 added new website
haftmann
parents:
diff changeset
    34
      <p>Isabelle is a joint project between Lawrence C. Paulson
e634d33deb86 added new website
haftmann
parents:
diff changeset
    35
      (University of Cambridge, UK) and Tobias Nipkow (Technical
e634d33deb86 added new website
haftmann
parents:
diff changeset
    36
      University of Munich, Germany).</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    37
16296
f05c81817ec6 refinements
haftmann
parents: 16284
diff changeset
    38
      <h2>Preview on Isabelle</h2>
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
    39
16296
f05c81817ec6 refinements
haftmann
parents: 16284
diff changeset
    40
        <a href="//media/pg_preview.mov">
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
    41
            <img class="left" src="//img/isabelle_pg_screenshot_small.png" alt="Sreenshot "
e634d33deb86 added new website
haftmann
parents:
diff changeset
    42
                width="250" height="277" />
e634d33deb86 added new website
haftmann
parents:
diff changeset
    43
        </a>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    44
16296
f05c81817ec6 refinements
haftmann
parents: 16284
diff changeset
    45
        <p>Here is a <a href="//media/pg_preview.mov">hyperlinked preview</a> demonstrating
f05c81817ec6 refinements
haftmann
parents: 16284
diff changeset
    46
        Isabelle and ProofGeneral, in <a href="http://www.apple.com/quicktime/download/">QuickTime
f05c81817ec6 refinements
haftmann
parents: 16284
diff changeset
    47
        format</a>, and also as a <a href="//media/pg_preview.pdf">non-hyperlinked preview</a> in PDF.</p>
f05c81817ec6 refinements
haftmann
parents: 16284
diff changeset
    48
        <br clear="all"/>
f05c81817ec6 refinements
haftmann
parents: 16284
diff changeset
    49
f05c81817ec6 refinements
haftmann
parents: 16284
diff changeset
    50
      <h2>What Isabelle offers</h2>
f05c81817ec6 refinements
haftmann
parents: 16284
diff changeset
    51
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
    52
      <p>Isabelle provides excellent notational support: new notations
e634d33deb86 added new website
haftmann
parents:
diff changeset
    53
      can be introduced, using normal mathematical symbols. Proofs can
e634d33deb86 added new website
haftmann
parents:
diff changeset
    54
      be written in a structured notation based upon traditional proof
e634d33deb86 added new website
haftmann
parents:
diff changeset
    55
      style, or more straightforwardly as sequences of
e634d33deb86 added new website
haftmann
parents:
diff changeset
    56
      commands. Definitions and proofs may include TeX source, from
e634d33deb86 added new website
haftmann
parents:
diff changeset
    57
      which Isabelle can automatically generate typeset documents.</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    58
e634d33deb86 added new website
haftmann
parents:
diff changeset
    59
      <p>The main limitation of all such proof systems is that proving
e634d33deb86 added new website
haftmann
parents:
diff changeset
    60
      theorems requires much effort from an expert user. Isabelle
e634d33deb86 added new website
haftmann
parents:
diff changeset
    61
      incorporates some tools to improve the user's productivity by
e634d33deb86 added new website
haftmann
parents:
diff changeset
    62
      automating some parts of the proof process. In particular,
e634d33deb86 added new website
haftmann
parents:
diff changeset
    63
      Isabelle's <em>classical reasoner</em> can perform long chains
e634d33deb86 added new website
haftmann
parents:
diff changeset
    64
      of reasoning steps to prove formulas. The <em>simplifier</em>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    65
      can reason with and about equations. Linear <em>arithmetic</em>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    66
      facts are proved automatically.</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    67
e634d33deb86 added new website
haftmann
parents:
diff changeset
    68
      <p>Isabelle comes with a large theory library of formally
e634d33deb86 added new website
haftmann
parents:
diff changeset
    69
      verified mathematics, including elementary number theory (for
e634d33deb86 added new website
haftmann
parents:
diff changeset
    70
      example, Gauss's law of quadratic reciprocity), analysis (basic
e634d33deb86 added new website
haftmann
parents:
diff changeset
    71
      properties of limits, derivatives and integrals), algebra (up to
e634d33deb86 added new website
haftmann
parents:
diff changeset
    72
      Sylow's theorem) and set theory (the relative consistency of the
e634d33deb86 added new website
haftmann
parents:
diff changeset
    73
      Axiom of Choice). Also provided are numerous examples arising
e634d33deb86 added new website
haftmann
parents:
diff changeset
    74
      from research into formal verification.</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    75
e634d33deb86 added new website
haftmann
parents:
diff changeset
    76
      <p>With <em>Isar</em>, Isabelle offers a concise proof formulation language
e634d33deb86 added new website
haftmann
parents:
diff changeset
    77
      which enables a user to write proof scripts naturally understandable for
e634d33deb86 added new website
haftmann
parents:
diff changeset
    78
      both humans <em>and</em> computers.</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    79
      
e634d33deb86 added new website
haftmann
parents:
diff changeset
    80
      <p>Isabelle is closely integrated with the <a href=
e634d33deb86 added new website
haftmann
parents:
diff changeset
    81
      "http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> user interface, which
e634d33deb86 added new website
haftmann
parents:
diff changeset
    82
      eases the task of writing and maintaining proof scripts.</p>
16240
95cc0e8f8a17 added shellcmd style
haftmann
parents: 16233
diff changeset
    83
      <br clear="all" />
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
    84
e634d33deb86 added new website
haftmann
parents:
diff changeset
    85
      <p>Ample <a href="dist/documentation.html">documentation</a> is available
e634d33deb86 added new website
haftmann
parents:
diff changeset
    86
      about using Isabelle and its inner concepts, including a
e634d33deb86 added new website
haftmann
parents:
diff changeset
    87
      <a href="http://www4.in.tum.de/~nipkow/LNCS2283/">Tutorial</a> published by
e634d33deb86 added new website
haftmann
parents:
diff changeset
    88
      Springer-Verlag.</p>
16296
f05c81817ec6 refinements
haftmann
parents: 16284
diff changeset
    89
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
    90
      <h2>Projects</h2>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    91
e634d33deb86 added new website
haftmann
parents:
diff changeset
    92
      <p>There is an (incomplete) list of past and present <a href=
e634d33deb86 added new website
haftmann
parents:
diff changeset
    93
      "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/projects.html">projects</a>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    94
      undertaken using Isabelle available.</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    95
e634d33deb86 added new website
haftmann
parents:
diff changeset
    96
      <h2>License</h2>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    97
          
e634d33deb86 added new website
haftmann
parents:
diff changeset
    98
      <p>Isabelle is distributed free of charge under the open source
16284
8bcecefd2e89 link bugs fixed
haftmann
parents: 16283
diff changeset
    99
      <!--a href="//dist/packages/Isabelle/COPYRIGHT"-->BSD license<!--/a-->. You may use any of our <a
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
   100
      href="dist/index.html">mirrors</a> for download.</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   101
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
   102
    </div>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   103
    <div class="hr"><hr/></div>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   104
    <?include file="//include/footer.include.html"?>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   105
</body>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   106
e634d33deb86 added new website
haftmann
parents:
diff changeset
   107
</html>