This repository has been archived by the owner on Nov 29, 2021. It is now read-only.
The LEO-II System Distribution
LEO-II is an interactive and automated higher-order theorem prover for classical higher-order logic (simple type theory).
LEO-II System Requirements: LEO-II runs on a regular Unix platform.
The following additional software is required:
- OCaml version 4.01.0 (other versions are untested; versions > 4.01.0 do, most likely, not work!)
- GNU bash, version 2.x or above
- A First Order Theorem Prover: Currently we recommend:
'The E Equational Theorem Prover' which is available at
http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html - GCC (to compile MiniSat backend)
LEO-II Installation and Usage: see the file INSTALL
LEO-II Further Information:
www.leoprover.org
mail: Christoph Benzmueller, c.benzmueller (at) googlemail.com