lib/html/library_index_content.template
author wenzelm
Sun May 18 17:01:31 2014 +0200 (2014-05-18)
changeset 56987 9b6628f29def
parent 51420 9cf33e987f0b
child 62191 eb9f5ee249f9
permissions -rw-r--r--
clarified dependencies -- Mavericks presently does not work;
haftmann@25235
     1
  <ul>
haftmann@25235
     2
    <li>Higher-Order Logic</li>
haftmann@25235
     3
haftmann@25235
     4
    <li style="list-style: none">
haftmann@25235
     5
      <ul>
haftmann@28307
     6
        <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
haftmann@28307
     7
        is a version of classical higher-order logic resembling
haftmann@28307
     8
        that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
haftmann@28307
     9
        </li>
haftmann@25235
    10
      </ul>
haftmann@25235
    11
    </li>
haftmann@25235
    12
  </ul>
haftmann@25235
    13
haftmann@25235
    14
  <ul>
haftmann@25235
    15
    <li>First-Order Logic</li>
haftmann@25235
    16
haftmann@25235
    17
    <li style="list-style: none">
haftmann@25235
    18
      <ul>
haftmann@28307
    19
        <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
haftmann@28307
    20
        provides basic classical and intuitionistic first-order logic. It is
haftmann@28307
    21
        polymorphic.
haftmann@28307
    22
        </li>
haftmann@25235
    23
haftmann@28307
    24
        <li><a href="ZF/index.html">ZF (Set Theory)</a>
haftmann@28307
    25
        offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
haftmann@28307
    26
        </li>
haftmann@25235
    27
haftmann@25235
    28
        <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>
haftmann@25235
    29
haftmann@25235
    30
        <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>
haftmann@25235
    31
haftmann@25235
    32
        <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
haftmann@25235
    33
      </ul>
haftmann@25235
    34
    </li>
haftmann@25235
    35
  </ul>
haftmann@25235
    36
haftmann@25235
    37
  <ul>
haftmann@25235
    38
    <li>Miscellaneous</li>
haftmann@25235
    39
haftmann@25235
    40
    <li style="list-style: none">
haftmann@25235
    41
      <ul>
haftmann@25235
    42
        <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
haftmann@25235
    43
haftmann@28307
    44
        <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
haftmann@28307
    45
        is an extensional version of Martin-L&ouml;f's Type Theory.</li>
haftmann@25235
    46
haftmann@25235
    47
        <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
haftmann@25235
    48
      </ul>
haftmann@25235
    49
    </li>
haftmann@25235
    50
  </ul>
haftmann@25235
    51