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.02 or above, including OCaml 5.  No preprocessor is
     needed: since 1.8.0 the build uses no camlp4.
   - GNU bash, version 2.x or above
   - A First Order Theorem Prover: Currently we recommend:  
      'The E Equational Theorem Prover' which is available at 
      https://github.com/eprover/eprover
   - 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