| author | wenzelm |
| Wed, 18 Dec 1996 12:46:59 +0100 | |
| changeset 2436 | 5be639c601b2 |
| parent 2084 | 5963238bc1b6 |
| permissions | -rw-r--r-- |
| clasohm@1311 | 1 |
<HTML><HEAD><TITLE>Isabelle Logics</TITLE></HEAD> |
| nipkow@1773 | 2 |
<center> |
| nipkow@1774 | 3 |
<H2> |
| nipkow@1774 | 4 |
<img src="Tools/Isabelle.gif"><P> |
| nipkow@1774 | 5 |
<i>The Logical Choice!</i> |
| nipkow@1774 | 6 |
</H2> |
| nipkow@1773 | 7 |
</center> |
| nipkow@1773 | 8 |
<P> |
| clasohm@1311 | 9 |
Click on the logic's name to view a list of its theories. |
| clasohm@1311 | 10 |
<HR> |
| clasohm@1311 | 11 |
First-Order Logic |
| paulson@2084 | 12 |
<UL> |
| paulson@2084 | 13 |
<LI><A HREF = "FOL/index.html">FOL</A> |
| paulson@2084 | 14 |
<LI><A HREF = "ZF/index.html">ZF (Set Theory)</A> |
| paulson@2084 | 15 |
<LI><A HREF = "CCL/index.html">CCL (Classical Computational Logic)</A> |
| paulson@2084 | 16 |
<LI><A HREF = "LCF/index.html">LCF (Logic of Computable Functions)</A> |
| paulson@2084 | 17 |
<LI><A HREF = "FOLP/index.html">FOLP (FOL with Proof Terms)</A> |
| paulson@2084 | 18 |
</UL> |
| clasohm@1311 | 19 |
<HR> |
| clasohm@1311 | 20 |
Higher-Order Logic |
| paulson@2084 | 21 |
<UL> |
| paulson@2084 | 22 |
<LI><A HREF = "HOL/index.html">HOL</A> |
| paulson@2084 | 23 |
<LI><A HREF = "HOLCF/index.html">HOLCF |
| paulson@2084 | 24 |
(Higher-Order Logic of Computable Functions)</A> |
| paulson@2084 | 25 |
</UL> |
| clasohm@1311 | 26 |
<HR> |
| clasohm@1311 | 27 |
Miscellaneous |
| paulson@2084 | 28 |
<UL> |
| paulson@2084 | 29 |
<LI><A HREF = "Sequents/index.html">Sequents |
| paulson@2084 | 30 |
(first-order, modal and linear logics)</A> |
| paulson@2084 | 31 |
<LI><A HREF = "CTT/index.html">CTT (Constructive Type Theory)</A> |
| paulson@2084 | 32 |
<LI><A HREF = "Cube/index.html">Cube (The Lambda Cube)</A> |
| paulson@2084 | 33 |
</UL> |
| clasohm@1311 | 34 |
<HR> |
| clasohm@1311 | 35 |
</BODY></HTML> |