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 or above - 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