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