lib/html/library_index_content.template
author wenzelm
Wed, 03 Nov 2021 12:04:22 +0100
changeset 74670 b2604cd4d131
child 74676 d37b204e1f89
permissions -rw-r--r--
recover library_index_content.template from c337c798f64c: required for website/build/main;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
74670
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
     1
  <ul>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
     2
    <li>Higher-Order Logic</li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
     3
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
     4
    <li style="list-style: none">
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
     5
      <ul>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
     6
        <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
     7
        is a version of classical higher-order logic resembling
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
     8
        that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
     9
        </li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    10
      </ul>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    11
    </li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    12
  </ul>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    13
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    14
  <ul>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    15
    <li>First-Order Logic</li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    16
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    17
    <li style="list-style: none">
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    18
      <ul>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    19
        <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    20
        provides basic classical and intuitionistic first-order logic. It is
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    21
        polymorphic.
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    22
        </li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    23
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    24
        <li><a href="ZF/index.html">ZF (Set Theory)</a>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    25
        offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    26
        </li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    27
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    28
        <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    29
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    30
        <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    31
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    32
        <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    33
      </ul>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    34
    </li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    35
  </ul>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    36
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    37
  <ul>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    38
    <li>Miscellaneous</li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    39
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    40
    <li style="list-style: none">
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    41
      <ul>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    42
        <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    43
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    44
        <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    45
        is an extensional version of Martin-L&ouml;f's Type Theory.</li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    46
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    47
        <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    48
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    49
        <li><a href="Pure/index.html">The Pure logical framework</a></li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    50
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    51
        <li><a href="Doc/index.html">Sources of Documentation</a></li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    52
      </ul>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    53
    </li>
b2604cd4d131 recover library_index_content.template from c337c798f64c: required for website/build/main;
wenzelm
parents:
diff changeset
    54
  </ul>