lib/html/library_index_content.template
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 51420 9cf33e987f0b
child 62191 eb9f5ee249f9
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);

  <ul>
    <li>Higher-Order Logic</li>

    <li style="list-style: none">
      <ul>
        <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
        is a version of classical higher-order logic resembling
        that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
        </li>
      </ul>
    </li>
  </ul>

  <ul>
    <li>First-Order Logic</li>

    <li style="list-style: none">
      <ul>
        <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
        provides basic classical and intuitionistic first-order logic. It is
        polymorphic.
        </li>

        <li><a href="ZF/index.html">ZF (Set Theory)</a>
        offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
        </li>

        <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>

        <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>

        <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
      </ul>
    </li>
  </ul>

  <ul>
    <li>Miscellaneous</li>

    <li style="list-style: none">
      <ul>
        <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>

        <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
        is an extensional version of Martin-L&ouml;f's Type Theory.</li>

        <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
      </ul>
    </li>
  </ul>