LEO-II 1.7.0

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