README

--------------------iProver-----------------------

iProver is a reasoner for first-order logic.

-------------------------------------------------
Download the current version from:
 
http://code.google.com/p/iprover/

-------------------------------------------------
                    Easy to install:
-------------------------------------------------

We assume OCaml v4.00 >= is installed. 

1) ./configure
2) make 

will produce executable: iproveropt


-1) "make clean"     to remove created objects and executable files
-2) "make clean_all" to remove created objects and executable files including E objects (if iProver does not compile try this first)

-------------------------------------------------
                    Easy to use: 
-------------------------------------------------

iproveropt problem.p

where problem.p is a problem in the TPTP format

-------------------------------------------------
                    Examples:
-------------------------------------------------

General:

1) iproveropt problem.p

Sat modes:

2) iproveropt --schedule sat problem_sat.p

3) iproveropt --sat_mode true --schedule none --sat_finite_models true problem_sat.p

FOF format:

4a) iproveropt --clausifier /home/eprover/eprover \
                --clausifier_options " --tstp-format --silent --cnf " problem_fof.p

  Clausifier is any executable that transforms formulas into TPTP cnf form, 
  --clausifier_options are the options passed to the clausifier. 
  If you are using bundled version then you do not need to specify these options.

4b)  iproveropt --clausifier /home/vampire/vampire --clausifier_options "--mode clausify"  problem_fof.p

5) iproveropt --help



-------------------------------------------------

It might be convenient to collect options you like in a file 
(e.g. example.opt) and run 

iproveropt $(cat example.opt) problem.p

The default options should be generally ok.


-----------------------------------------------------
                   Output
----------------------------------------------------

Output: the output of iProver is according to a modified version of SZS ontology:

"SZS status Theorem"  
                       corresponds to a proved theorem where 
                       the input is first-order and contains 
                       a theorem represented by a conjecture.

"SZS status CounterSatisfiable" 
	               corresponds to disproving the theorem where
                       the input is first-order and contains 
                       a theorem represented by a conjecture. 

"SZS status Unsatisfiable"
                       corresponds to an unsatisfiable set of input formulas                     
                       where the input does not contain a theorem 
                       (i.e. either cnf or fof and does not contain a conjecture)	

"SZS status Satisfiable"
                       corresponds to a satisfiable set of input formulas
                       where the input does not contain a theorem
                       (i.e. contains neither a conjecture or a negated_conjecture)



% SZS output start Model  Model representation output 
                          when a model is found by instantiation
% SZS output end Model 

--------------------------------------------------------------------------------------------
Please send any comments, report bugs to korovin[@]cs.man.ac.uk
If you are interested in a different from GNU GPL license please email korovin[@]cs.man.ac.uk
--------------------------------------------------------------------------------------------

-------------------------------------------------
            Additional Info
-------------------------------------------------              

iProver is based on an instantiation calculus Inst-Gen, 
which is complete for first-order logic:
http://www.cs.man.ac.uk/~korovink/my_pub/instantiation_lics03.ps

iProver has been developed and implemented by 
Konstantin Korovin (korovin[@]cs.man.ac.uk), 
The University of Manchester, UK
In 2008 Christoph Sticksel has joined the project.

iProver combines instantiation with resolution and implements a number 
of redundancy elimination methods:
http://www.cs.man.ac.uk/~korovink/my_pub/inv_to_inst.ps
(see also the list of options for details)

For ground reasoning iProver uses C version of MiniSat:
http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/

iProver accepts problems in TPTP format:
http://www.cs.miami.edu/~tptp/

For problems in fof (and not just cnf) format, 
iProver can use any external clausifier, see examples.


External clausifier is NOT required if the input is in cnf and 
a clausifier (as an option to E prover) 
is included only in the bundled distribution.

iProver has a satisfiability mode which includes a finite model finder, 
incorporating some ideas from Paradox and DarwinFM.

To activate satisfiability mode use "iproveropt --sat_mode true problem_sat.p".
to search for finite models you can run 
"iproveropt --sat_mode true --schedule none --sat_finite_models true problem_sat.p".

iProver outputs models when satisfiability is shown  by instantiation. 
Different representations of models are implemented 
based on definitions of predicates in term algebra.
 

-----------------------------------------------------
iProver combines instantiation with resolution 

If you would like to run pure instantiation/resolution 
then you can switch the corresponding flag 
(see -help for all options)


-----------------------------------------------------
External libraries (freely available with LGPL compatible licenses) are: 

MiniSat by Niklas Een and Niklas Sorensson
Heaps   by Jean-Christophe Filliatre

You can replace default solver MiniSAT with 

PicoSAT developed by Armin Biere  using 
"make PicoSAT=true"  

Lingeling  developed by Armin Biere using 
"make LGL=true"