lib/html/library_index_content.template
 author wenzelm Mon, 17 May 2010 23:54:15 +0200 changeset 36960 01594f816e3a parent 28307 39328b6ea7e8 child 40776 cce37f6d4b69 permissions -rw-r--r--
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax; eliminated old-style structure aliases K = Keyword, P = Parse;
```
<ul>
<li>Higher-Order Logic</li>

<li style="list-style: none">
<ul>
<li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
is a version of classical higher-order logic resembling
that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
</li>

<li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a>
adds Scott's Logic for Computable Functions (domain theory) to HOL.
</li>
</ul>
</li>
</ul>

<ul>
<li>First-Order Logic</li>

<li style="list-style: none">
<ul>
<li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
provides basic classical and intuitionistic first-order logic. It is
polymorphic.
</li>

<li><a href="ZF/index.html">ZF (Set Theory)</a>
offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
</li>

<li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>

<li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>

<li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
</ul>
</li>
</ul>

<ul>
<li>Miscellaneous</li>

<li style="list-style: none">
<ul>
<li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>

<li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
is an extensional version of Martin-L&ouml;f's Type Theory.</li>

<li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
</ul>
</li>
</ul>

```