THE LEO-II System Installation Guide
(Christoph Benzmueller)

NOTE: 
  Version 0.97 now also runs under Objective Caml release 3.10
  Versions 0.95 and 0.9 only run under Objective Caml release 3.09

LEO-II Installation Instructions:

 (1) Choose an [installation-directory], e.g. /home/chris/
 (2) Download leo2.tgz from 
         http://www.ags.uni-sb.de/~chris/leo/leo2-v***.tgz 
     and store it in 
                   [installation-directory]
 (3) change to the installation directory
                   cd [installation-directory]
      
 (4) extract the files of the packages
                   tar xzf leo2-v***.tgz
 (5) change to the main source directory of the LEO-II package
                   cd [installation-directory]/leo2/src

 (6a) compile the LEO-II sources 
                   make opt
     this creates the executable
                   [installation-directory]/leo2/bin/leo.opt

 alternatively you may try 

 (6b) compile the LEO-II sources 
                   make all
     this creates the executable
                   [installation-directory]/leo2/bin/leo

Enabling the cooperation of LEO-II with at least one First-Order Prover:
  
 - LEO-II is designed to cooperate with first-order provers. Thus installation 
   of a first order prover is crucial in order to run LEO-II. While LEO-II
   can cooperate with different first-order provers, we recommend here to 
   install the 'The E Equational Theorem Prover' which is available at 
   http://www4.informatik.tu-muenchen.de/~schulz/WORK/eprover.html
 - In the following we assume that the binary for running prover E is available
   in file 
                    [eprover-directory]/eprover
 - In order to inform LEO-II where it can find this binary for E you need to 
   provide a file 
                    [your-homedirectory]/.leoatprc
   containing the following entry:
                    e = [eprover-directory]/eprover


Running LEO-II in Automatic Modus:

 - To start LEO-II you need to type: 
                    [installation-directory]/leo2/bin/leo.opt
     or 
                    [installation-directory]/leo2/bin/leo

     Usage:  [installation-directory]/leo2/bin/leo[.opt] [OPTIONS] [FILE]

     Options:
     --help, -h                 Display this help screen
     --version, -v             Display version information
     --foatp PROVER, -f PROVER  Use PROVER as first-order prover
              Currently supported: e, spass
              Default prover is e
     --dir DIR, -d DIR          Run on all files in DIR
     --interactive, -i            Start interactive mode
              Default is non-interactive
     --debug N, -D N          Set debug level to N
               (0 = no output, 1 = minimal output, 2 = full output)
               Default: 0

 - Example: 
    [installation-directory]/leo2/bin/leo -d [installation-directory]/leo2/demoarea -f e 
  
   (please make sure that you have write permissions for [installation-directory]/leo2/demoarea)

Running LEO-II in Intercative Modus:
   
 - To start LEO-II's command line interface type: 
                    [installation-directory]/leo2/bin/leo[.opt] -i
 - There is a help command 
                    help
   which provides an overview on all available commands of LEO-II.
 - In order to load a demofile type
                    read-problem-file  [installation-directory]/leo2/demoarea/SET171+3.thf
 - In order to automatically prove the problem type
                    prove-with-fo-atp e
 - In order to inspect the proof object for the derivation of the empty clause in this
   example type
                    show-derivation 63
   (63 is the number of the empty clause a signalled by LEO-II before)
- You may also want to run LEO-II on all examples in the demoarea directory:
                    prove-directory-with-fo-atp [installation-directory]/leo2/demoarea/ e

   (please make sure that you have write permissions for [installation-directory]/leo2/demoarea)