equal
deleted
inserted
replaced
|
1 <ul> |
|
2 <li>Higher-Order Logic</li> |
|
3 |
|
4 <li style="list-style: none"> |
|
5 <ul> |
|
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> |
|
10 </ul> |
|
11 </li> |
|
12 </ul> |
|
13 |
|
14 <ul> |
|
15 <li>First-Order Logic</li> |
|
16 |
|
17 <li style="list-style: none"> |
|
18 <ul> |
|
19 <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a> |
|
20 provides basic classical and intuitionistic first-order logic. It is |
|
21 polymorphic. |
|
22 </li> |
|
23 |
|
24 <li><a href="ZF/index.html">ZF (Set Theory)</a> |
|
25 offers a formulation of Zermelo-Fraenkel set theory on top of FOL. |
|
26 </li> |
|
27 |
|
28 <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li> |
|
29 |
|
30 <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li> |
|
31 |
|
32 <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li> |
|
33 </ul> |
|
34 </li> |
|
35 </ul> |
|
36 |
|
37 <ul> |
|
38 <li>Miscellaneous</li> |
|
39 |
|
40 <li style="list-style: none"> |
|
41 <ul> |
|
42 <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li> |
|
43 |
|
44 <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a> |
|
45 is an extensional version of Martin-Löf's Type Theory.</li> |
|
46 |
|
47 <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li> |
|
48 |
|
49 <li><a href="Pure/index.html">The Pure logical framework</a></li> |
|
50 |
|
51 <li><a href="Doc/index.html">Sources of Documentation</a></li> |
|
52 </ul> |
|
53 </li> |
|
54 </ul> |