Admin/website/logics.html
author haftmann
Sun, 05 Jun 2005 14:33:02 +0200
changeset 16275 951803bff5b1
parent 16272 bcf05183df9e
child 16575 15d5f8e729fe
permissions -rw-r--r--
a more spohisticated symlink handling
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>Logics</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>Isabelle's Logics</h2>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    18
      <p>Isabelle can be viewed from two main
e634d33deb86 added new website
haftmann
parents:
diff changeset
    19
      perspectives. On the one hand it may serve as a generic framework for rapid
e634d33deb86 added new website
haftmann
parents:
diff changeset
    20
      prototyping of deductive systems. On the other hand, major existing logics
e634d33deb86 added new website
haftmann
parents:
diff changeset
    21
      like <a href="#isabelle_hol"><em>Isabelle/HOL</em></a>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    22
      provide a theorem proving environment
e634d33deb86 added new website
haftmann
parents:
diff changeset
    23
      ready to use for sizable applications.</p>    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    24
      
e634d33deb86 added new website
haftmann
parents:
diff changeset
    25
      <p>The Isabelle distribution includes a large body of
e634d33deb86 added new website
haftmann
parents:
diff changeset
    26
      object logics and other examples (see the <a href=
e634d33deb86 added new website
haftmann
parents:
diff changeset
    27
      "library/index.html">Isabelle theory library</a>).</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    28
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    29
      <dl>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    30
        <dt id="isabelle_hol"><a href="library/HOL/index.html">Isabelle/HOL</a></dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    31
        <dd>is a version of classical higher-order logic resembling that of the
e634d33deb86 added new website
haftmann
parents:
diff changeset
    32
        <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>. The
e634d33deb86 added new website
haftmann
parents:
diff changeset
    33
        main libraries of the HOL 4 System are now <a href=
e634d33deb86 added new website
haftmann
parents:
diff changeset
    34
        "library/HOL/HOL-Complex/HOL4/index.html">available in Isabelle</a>.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    35
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    36
        <dt><a href=
e634d33deb86 added new website
haftmann
parents:
diff changeset
    37
        "library/HOLCF/index.html">Isabelle/HOLCF</a></dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    38
        <dd>adds Scott's Logic for Computable Functions (domain theory) to
e634d33deb86 added new website
haftmann
parents:
diff changeset
    39
        HOL.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    40
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    41
        <dt><a href="library/FOL/index.html">Isabelle/FOL</a></dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    42
        <dd>provides basic classical and intuitionistic first-order logic. It is
e634d33deb86 added new website
haftmann
parents:
diff changeset
    43
        polymorphic.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    44
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    45
        <dt><a href="library/ZF/index.html">Isabelle/ZF</a></dt>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    46
            <dd>offers a formulation of Zermelo-Fraenkel set theory on top of FOL.</dd>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    47
      </dl>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    48
e634d33deb86 added new website
haftmann
parents:
diff changeset
    49
      <p><em>Isabelle/HOL</em> is currently the best developed object logic, including an
e634d33deb86 added new website
haftmann
parents:
diff changeset
    50
      extensive library of (concrete) mathematics, and various packages for
e634d33deb86 added new website
haftmann
parents:
diff changeset
    51
      advanced definitional concepts like (co-)inductive sets and types,
e634d33deb86 added new website
haftmann
parents:
diff changeset
    52
      well-founded recursion etc. The distribution also includes some large
e634d33deb86 added new website
haftmann
parents:
diff changeset
    53
      applications, for example correctness proofs of cryptographic protocols
e634d33deb86 added new website
haftmann
parents:
diff changeset
    54
      (<a href="library/HOL/Auth/index.html">HOL/Auth</a>) or communication
e634d33deb86 added new website
haftmann
parents:
diff changeset
    55
      protocols (<a href="library/HOLCF/IOA/index.html">HOLCF/IOA</a>).</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    56
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    57
      <p><em>Isabelle/ZF</em> provides another starting point for applications, with a
e634d33deb86 added new website
haftmann
parents:
diff changeset
    58
      slightly less developed library. Its definitional packages are similar to
e634d33deb86 added new website
haftmann
parents:
diff changeset
    59
      those of Isabelle/HOL. Untyped ZF provides more advanced constructions for
e634d33deb86 added new website
haftmann
parents:
diff changeset
    60
      sets than simply-typed HOL.</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    61
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    62
      <p>There are a few minor object logics that may serve as further examples:
e634d33deb86 added new website
haftmann
parents:
diff changeset
    63
      <a href="library/CTT/index.html">CTT</a> is an extensional version of
e634d33deb86 added new website
haftmann
parents:
diff changeset
    64
      Martin-L&ouml;f's Type Theory, <a href="library/Cube/index.html">Cube</a> is
e634d33deb86 added new website
haftmann
parents:
diff changeset
    65
      Barendregt's Lambda Cube. There are also some sequent calculus examples under
e634d33deb86 added new website
haftmann
parents:
diff changeset
    66
      <a href="library/Sequents/index.html">Sequents</a>, including modal and
e634d33deb86 added new website
haftmann
parents:
diff changeset
    67
      linear logics. Again see the <a href="library/index.html">Isabelle theory
e634d33deb86 added new website
haftmann
parents:
diff changeset
    68
      library</a> for other examples.</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    69
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    70
      <h2>Defining Logics</h2>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    71
e634d33deb86 added new website
haftmann
parents:
diff changeset
    72
      <p>Logics are not hard-wired into Isabelle, but
e634d33deb86 added new website
haftmann
parents:
diff changeset
    73
      formulated within Isabelle's meta logic: <em>Isabelle/Pure</em>.
e634d33deb86 added new website
haftmann
parents:
diff changeset
    74
      There are quite a lot of syntactic and deductive tools available in generic
e634d33deb86 added new website
haftmann
parents:
diff changeset
    75
      Isabelle. Thus defining new logics or extending existing ones basically works
e634d33deb86 added new website
haftmann
parents:
diff changeset
    76
      as follows:</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    77
    
e634d33deb86 added new website
haftmann
parents:
diff changeset
    78
      <ol>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    79
        <li>declare concrete syntax (via mixfix grammar and syntax macros)</li>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    80
        <li>declare abstract syntax (as higher-order constants)</li>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    81
        <li>declare inference rules (as meta-logical propositions)</li>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    82
        <li>instantiate generic automatic proof tools (simplifier, classical
e634d33deb86 added new website
haftmann
parents:
diff changeset
    83
        tableau prover etc.)</li>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    84
        <li>manually code special proof procedures (via tacticals or hand-written
e634d33deb86 added new website
haftmann
parents:
diff changeset
    85
        ML)</li>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    86
      </ol>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    87
      
e634d33deb86 added new website
haftmann
parents:
diff changeset
    88
      <p>The first three steps above are fully declarative and involve no ML
e634d33deb86 added new website
haftmann
parents:
diff changeset
    89
      programming at all. Thus one already gets a decent deductive environment
e634d33deb86 added new website
haftmann
parents:
diff changeset
    90
      based on primitive inferences (by employing the built-in mechanisms of
e634d33deb86 added new website
haftmann
parents:
diff changeset
    91
      <em>Isabelle/Pure</em>, in particular higher-order unification and resolution). For
e634d33deb86 added new website
haftmann
parents:
diff changeset
    92
      sizable applications some degree of automated reasoning is essential.
e634d33deb86 added new website
haftmann
parents:
diff changeset
    93
      Instantiating existing tools like the classical tableau prover involves only
e634d33deb86 added new website
haftmann
parents:
diff changeset
    94
      minimal ML-based setup. One may also write arbitrary proof procedures or even
16272
schirmer
parents: 16240
diff changeset
    95
      theory extension packages in ML, without breaking system soundness (Isabelle
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
    96
      follows the well-known <em>LCF system approach</em> to achieve a secure
e634d33deb86 added new website
haftmann
parents:
diff changeset
    97
      system).</p>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    98
    </div>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    99
    <div class="hr"><hr/></div>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   100
    <?include file="//include/footer.include.html"?>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   101
</body>
e634d33deb86 added new website
haftmann
parents:
diff changeset
   102
e634d33deb86 added new website
haftmann
parents:
diff changeset
   103
</html>