KRH (currently) accepts only input in canonical Prolog syntax. This means that no declared infix or prefix operators can be used.
Auxiliary scripts can be used to filter input files or input streams that use Prolog standard operators.
Example: Canonicalization as file-to-file transformation :
$ canonicalize.pl myfile.tme >myfile_canonical.tme $ krh myfile_canonical.tme
Example: Canonicalization on the fly:
$ canonicalize.pl myfile.tme | krh -
Example: Interaction with KRH:
$ canfilter.pl | krh -tty -
Example: Interaction with KRH using a custom initialization file:
$ canfilter.pl | krh -tty krh_init.tme -
In the Hypertableau calculus, inferred disjuncts do not share variables.
The core proving program
krh does not ensure this.
pre.pl transforms an input clause set which
is non-Horn and not range restricted in such
a way, that disjuncts derived by
krh are ground.
Its output is canonical and can
be directly used as input to the
On Horn or range restricted inputs, this transformation has only the effect
of canonicalization. So
can in general be used in place of
For an example, see the TPTP Problem below.
Note: If reductions such as complement splitting are in effect, disjuncts must actually be ground.
krh verifies at runtime that derived disjuncts are
KRH can be used interactively within Emacs in Prolog mode.
You need a script that starts it with appropriate input filtering,
#! DIR=/lab/ki/local/intel-linux $DIR/lib/krh/scripts/canfilter.pl | $DIR/bin/krh -tty $HOME/.krh_emacs_init -
$HOME/.krh_emacs_init can contain KRH statements
that are to be executed each time when KRH is started within Emacs, for
#(set_message_output(stdout)). #(set_flag(proof_terms, true)).
.emacs file a command
can be defined as follows. (This may vary slightly for different
Prolog modes which are available for Emacs).
(defun run-krh () (interactive) (let ((prolog-program-name "/home/myself/bin/krh_emacs")) (run-prolog nil)))
proteinformat (file extension
.tme), as generated by the
tptp_before.tmeis used to configure settings, for example:
%%%% File tptp_before.tme #(clear_builtins). %% Avoid accidentals #(set_parameter(max_weight_initial, 3)). %% Good for TPTP stuff #(set_flag(proof_terms, true)). %% Activate level cut
tptp_after.tmeis used to start the prover, for example:
%%%% File tptp_after.tme #(run). %% Start proving #(onto_file([#(print_proof)], '/tmp/pr1.pl')). %% Output the proof term
$ pre.pl $TPTPDirectory/Problems/protein/MSC/MSC006-1.tme | krh tptp_before.tme - tptp_after.tme
a ; b. c ; d. false :- d. #run. #print_extent. #next. #print_extent. #next.
#(set_flag(proof_terms,true)).must be in the input before
#(run)and a command like
#(run). As a side effect of running the task a proof term is then printed to the file
$ proofs_to_dot.pl -tgif -d/tmp /tmp/pr1.pl $ xv /tmp/proof_00001.gif