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/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> 55