Download
Download the latest version of LEO-II. LEO-II is distributed under the BSD license (COPYRIGHT)
LEO-II Sources (installation instructions: INSTALL)
- LEO-II v1.7.0 (runs under OCaml 4.00) (leo2_v1.7.0.tgz)
- LEO-II v1.6.3 (runs under OCaml 4.00) (leo2_v1.6.3.tgz)
- LEO-II v1.6.2 (runs under OCaml 4.00) (leo2_v1.6.2.tgz)
- LEO-II v1.6.1 (runs under OCaml 4.00) (leo2_v1.6.1.tgz)
- LEO-II v1.6.0 (runs under OCaml 4.00) (leo2_v1.6.0.tgz)
- LEO-II v1.5.0 (runs under OCaml 4.00) (leo2_v1.5.0.tgz)
- LEO-II v1.4.3 (runs under OCaml 3.12) (leo2_v1.4.3.tgz)
- Please contact Christoph Benzmüller for older versions.
Example problems in TPTP THF syntax and example proof certificates in TPTP TSTP syntax
- Example problems in Quantified Conditional Logics (QCL):
- Embedding of QCLs in THF0: QCLAxioms.ax
- Example for meta-level reasoning; QCL axiom ID corresponds to a respective semantic condition on selection function f: ID_corr.p
- Example proof certificate of LEO-II for the previous theorem (without E subproof): ID_corr.proof.po1.txt
- Example proof certificate of LEO-II for the previous theorem (with integrated E subproof): ID_corr.proof.po2.txt
- TPTP library (all problems with a '^' in their name are THF)