author | paulson |
Thu, 10 Oct 1996 10:57:33 +0200 | |
changeset 2084 | 5963238bc1b6 |
parent 1774 | bc584c1b8426 |
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:
1774
diff
changeset
|
12 |
<UL> |
5963238bc1b6
New root file with more description, and merging LK and Modal to Sequents
paulson
parents:
1774
diff
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:
1774
diff
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:
1774
diff
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:
1774
diff
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:
1774
diff
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:
1774
diff
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:
1774
diff
changeset
|
21 |
<UL> |
5963238bc1b6
New root file with more description, and merging LK and Modal to Sequents
paulson
parents:
1774
diff
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:
1774
diff
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:
1774
diff
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:
1774
diff
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:
1774
diff
changeset
|
28 |
<UL> |
5963238bc1b6
New root file with more description, and merging LK and Modal to Sequents
paulson
parents:
1774
diff
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:
1774
diff
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:
1774
diff
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:
1774
diff
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:
1774
diff
changeset
|
33 |
</UL> |
1311 | 34 |
<HR> |
35 |
</BODY></HTML> |