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