changeset 16233 e634d33deb86
child 16240 95cc0e8f8a17
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/website/overview.html	Sat Jun 04 10:26:08 2005 +0200
@@ -0,0 +1,106 @@
+<?xml version='1.0' encoding='iso-8859-1' ?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "">
+<?cvs id="$Id$"?>
+<html xmlns="">
+    <title>Overview</title>
+    <?include file="//include/htmlheader.include.html"?>
+<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>What Isabelle offers</h2>
+        <a href="//img/isabelle_pg_screenshot_big.png">
+            <img class="left" src="//img/isabelle_pg_screenshot_small.png" alt="Sreenshot "
+                width="250" height="277" />
+        </a>
+      <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=
+      "">ProofGeneral</a> user interface, which
+      eases the task of writing and maintaining proof scripts.</p>
+      <br clear="both" />
+      <h2>Preview</h2>
+      <p>We provide a <a href="">hyperlinked preview</a> demonstrating
+      Isabelle and ProofGeneral, in <a href="">QuickTime
+      format</a>, and also as a <a href="PG-preview.pdf">non-hyperlinked preview</a> in PDF.</p>
+      <p>Ample <a href="dist/documentation.html">documentation</a> is available
+      about using Isabelle and its inner concepts, including a
+      <a href="">Tutorial</a> published by
+      Springer-Verlag.</p>
+      <h2>Projects</h2>
+      <p>There is an (incomplete) list of past and present <a href=
+      "">projects</a>
+      undertaken using Isabelle available.</p>
+      <h2>License</h2>
+      <p>Isabelle is distributed free of charge under the open source
+      <a href="dist/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"?>