Generating formulas for JProver
-------------------------------

The formulas for benchmarking JProver can be generated by the
tptp2X-tool (see ReadMe-File in the TPTP2X-directory).
However, the formulas for JProver must not contain Prolog-comments
(starting with %). So you may just copy tptp2X.main.no_comments to
tptp2X.main.

Installing JProver
------------------

JProver is (still) integrated within MetaPRL, an interactive proof
environment (http://www.metaprl.org). So you have to install MetaPRL,
which requires OCaml and OMake.
We benchmarked JProver by calling the function "gen_prover" in the
module "Jall" (file metaprl/refiner/reflib/jall.ml). This function
call may occur e.g. in the module "Itt_logic"
(metaprl/theories/itt/core/itt_logic.ml), which can be loaded in the 
editor of MetaPRL. The proof transformation we commented out in order
to test finding the proof only. 
In the following are more detailed suggestions:

1. Download MetaPRL from http://www.metaprl.org
   We used MetaPRL-SVN-2005.11.27 (v.0.9.6.4+) at http://files.metaprl.org/.
   You also need Ocaml and OMake (we used OCaml 3.09 and OMake 0.9.6.)

2. untar and uncompress MetaPrl:
   tar -xjf MetaPRL-SVN-2005.11.27.tar.bz2

3. cd metaprl
   omake
   (that creates file metaprl/mk/config)

4. Edit metaprl/mk/config: 
   set parameters as you wish
   (we set COMPILATION_MODE = native)

5. For mor convenient benchmarking adapt the modules Itt_logic and Jall:

In metaprl/theories/itt/core/itt_logic.ml insert:

let prover mult_lim calc hyps concls = 
  let mult_limit = if mult_lim = 0 then None else Some mult_lim in
  let calculus = match calc with
  | "J" -> (Intuit SingleConcl)
  | "C" -> Classical
  | _ -> raise (Invalid_argument "ITT_JProver.gen_prover calculus")
  in
  let start = Unix.times () in
  match 
    ITT_JProver.gen_prover mult_limit calculus hyps concls 
  with     
    empty_inf ->
      begin
	let finish = Unix.times () in
	let duration = (finish.Unix.tms_utime +. finish.Unix.tms_cutime) -. 
	    (start.Unix.tms_utime +. start.Unix.tms_cutime) in 
	printf "%g s\n" duration; 
        flush stdout;
      end

let prove concl = prover 0 "J" [] [concl]

(* example formula *)
let f = << all x. 'p['x] and exst y. 'q['y] => exst z. ('p['z] or not{'q['z]}) >>

In metaprl/theories/itt/core/itt_logic.mli insert:

topval prover : int -> string -> term list -> term list -> unit
topval prove : term -> unit
topval f : term

In metaprl/refiner/reflib/jall.ml replace the original definition of
function "gen_prover" by:

let gen_prover mult_limit calculus hyps concls =
	(* rev_append on the next line would break some proofs *)
   let consts =
		renam_free_vars SymbolSet.empty hyps
	in
   let consts =
      renam_free_vars consts concls
   in
   let _ftree, _red_ordering, (_sigmaQ,_sigmaJ), _ext_proof =
		prove consts mult_limit hyps concls calculus
	in
	if calculus = S4 then
		eprintf "matrix proof found@.";
   (* without transformation into sequent proof *)
   (* let red_ordering = PMap.fold (fun acc p s -> (p,s)::acc) [] red_ordering in *)
   (* it's too early to convert ext_proof to a set *)
   (* let sequent_proof = reconstruct ftree red_ordering sigmaQ ext_proof calculus consts in *)
         (* transform types let rename constants *)
     (* we can transform the eigenvariables AFTER proof reconstruction since *)
     (* new delta_0 constants may have been constructed during rule permutation *)
     (* from the LJmc to the LJ proof *)
   (* create_output consts sequent_proof *)
   JLogic.empty_inf


6. cd metaprl
   omake
   
   This gives a lot of output. If it failes you may have to choose
   other parameters in the file config, or contact us.

7. Start MetaPRL-Editor:
   cd metaprl/editor/ml
   a) interactive:

   ./mpxterm &

   prompt in the editor:

   cd "itt_logic";;
   f;;        
   prove f;;  
   exit ();;        

   or 
   b) non-interactive:

   create a file "metaprl/editor/ml/jptest.ml" which contains these
   directives: 

   cd "itt_logic";;
   f;;        
   prove f;;  
   exit ();; 

   ./mpopt -cli jptest.ml