CASC ReadMe



Running E-KRHyper in CASC - regular (non-LTB) divisions:

   For CASC E-KRHyper accepts CNF and FOF input in TPTP-syntax.

   E-KRHyper is usually controlled with configuration files containing
   various flags and commands, and these files must be loaded into the prover
   together with the problem.
   For CASC this has been simplified: the user starts the shell script 
   'ekrhyper' (found in /usr/lib/e-krhyper/casc) with the problem file as its argument, 
   and the script then starts the prover and loads the the required files in the
   correct order. Thus the invocation is: 
   
   /usr/lib/e-krhyper/casc/ekrhyper %s
   
   where %s is the TPTP problem file, for example
   /usr/lib/e-krhyper/casc/ekrhyper ~/TPTP-v5.3.0/Problems/ALG/ALG011-1.p

   No other command line arguments are accepted. E-KRHyper will run until 
   it terminates on its own or is interrupted from the outside.
   
   (The 'ekrhyper' shell script corresponds to executing the following command:
   /usr/bin/ekrh /usr/lib/e-krhyper/casc/config.tme %s /usr/lib/e-krhyper/casc/run.tme)
   
   If E-KRHyper terminates, then the prover will print a line of SZS output to
   stdout:
   - for an unsatisfiable CNF/FOF problem:
   
    % SZS status Unsatisfiable
	
   - for a satisfiable CNF/FOF problem:

	% SZS status Satisfiable

   - for a FOF theorem:
	
	% SZS status Theorem
	
   - for a FOF problem with countersatisfiable conjecture:

	% SZS status CounterSatisfiable
	
Running E-KRHyper in CASC - LTB division:	

   In the LTB division E-KRHyper is run using the Perl script 'ekrhyper_ltb.pl'
   (found in /usr/lib/e-krhyper/casc). 
   The command line invocation is:
   
   /usr/lib/e-krhyper/casc/ekrhyper_ltb.pl %s %d
   
   ...where %s is the name of a batch file and %d is the total time limit.
   
   If any file paths in the batch specification are not absolute, then 
   E-KRHyper will look for these in the directory specified by the $TPTP 
   environment variable.
   E-KRHyper will print the results for the individual problems into the output
   files specified in the batch file. An individual result is either one of the
   SZS output lines described above, or it is
   
   % SZS status GaveUp
   
   ...if E-KRHyper could not solve a particular problem and moved on to the next
   one.
   If the batch specification states that answer output is desired or required,
   then E-KRHyper will attempt to compute answers for the respective problems.
   If the prover succeeds in this, then the answer(s) will be printed in 
   addition to the normal SZS output stated above, using SZS Tuple Answer syntax.
   Example:
   
   % SZS status Theorem
   % SZS answers Tuple [[a,b,c],[d,e,f]].
   
   The script will also print its progress to stdout. For each problem it will print
   
   % SZS status Started for <problem>
   
   as soon as it has started working on <problem>.
   Once it has finished that problem, it will print the result (same as in the output
   file) to stdout, followed by
   
   % SZS status Ended for <problem>
   
   Example:
   % SZS status Started for Problems/CSR/CSR083+3.p
   % SZS status Theorem
   % SZS answers Tuple [[s__Human]].
   % SZS status Ended for Problems/CSR/CSR083+3.p


Running EKRH webservice

   An experimental interface allows connecting ekrh to webservices which
   can then be accessed during reasoning via special literals, see the
   MANUAL.TXT for this as well. The interface is written in JAVA and
   found in the directory ekrh/loganswer_proxy
   Compile it with javac, after that it needs to be started as a separate 
   process. The interface process and ekrh communicate over a port. The
   default is for both to run on the same machine. See the MANUAL.TXT
   for changing these settings.
   The interface is developed by Markus Bender <mbender@uni-koblenz.de>.