lib/html/library_index_content.template
changeset 28307 39328b6ea7e8
parent 25235 04cb7e02ca38
child 40776 cce37f6d4b69
equal deleted inserted replaced
28306:e2f091391865 28307:39328b6ea7e8
     1   <ul>
     1   <ul>
     2     <li>Higher-Order Logic</li>
     2     <li>Higher-Order Logic</li>
     3 
     3 
     4     <li style="list-style: none">
     4     <li style="list-style: none">
     5       <ul>
     5       <ul>
     6         <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a></li>
     6         <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
       
     7         is a version of classical higher-order logic resembling
       
     8         that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
       
     9         </li>
     7 
    10 
     8         <li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a></li>
    11         <li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a>
       
    12         adds Scott's Logic for Computable Functions (domain theory) to HOL.
       
    13         </li>
     9       </ul>
    14       </ul>
    10     </li>
    15     </li>
    11   </ul>
    16   </ul>
    12 
    17 
    13   <ul>
    18   <ul>
    14     <li>First-Order Logic</li>
    19     <li>First-Order Logic</li>
    15 
    20 
    16     <li style="list-style: none">
    21     <li style="list-style: none">
    17       <ul>
    22       <ul>
    18         <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a></li>
    23         <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
       
    24         provides basic classical and intuitionistic first-order logic. It is
       
    25         polymorphic.
       
    26         </li>
    19 
    27 
    20         <li><a href="ZF/index.html">ZF (Set Theory)</a></li>
    28         <li><a href="ZF/index.html">ZF (Set Theory)</a>
       
    29         offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
       
    30         </li>
    21 
    31 
    22         <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>
    32         <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>
    23 
    33 
    24         <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>
    34         <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>
    25 
    35 
    33 
    43 
    34     <li style="list-style: none">
    44     <li style="list-style: none">
    35       <ul>
    45       <ul>
    36         <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
    46         <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
    37 
    47 
    38         <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a></li>
    48         <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
       
    49         is an extensional version of Martin-L&ouml;f's Type Theory.</li>
    39 
    50 
    40         <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
    51         <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
    41       </ul>
    52       </ul>
    42     </li>
    53     </li>
    43   </ul>
    54   </ul>