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.
The script 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 krh
program.
On Horn or range restricted inputs, this transformation has only the effect
of canonicalization. So pre.pl
can in general be used in place of
canonicalize.pl
.
For an example, see the TPTP Problem below.
Note: If reductions such as complement splitting are in effect, disjuncts must actually be ground.
Note:The flag check_disjunctions_are_ground
effects that krh
verifies at runtime that derived disjuncts are
ground.
KRH can be used interactively within Emacs in Prolog mode.
You need a script that starts it with appropriate input filtering,
for example $HOME/bin/krh_emacs
:
#! DIR=/lab/ki/local/intel-linux $DIR/lib/krh/scripts/canfilter.pl | $DIR/bin/krh -tty $HOME/.krh_emacs_init -
The file $HOME/.krh_emacs_init
can contain KRH statements
that are to be executed each time when KRH is started within Emacs, for
example:
#(set_message_output(stdout)). #(set_flag(proof_terms, true)).
Within the .emacs
file a command run-krh
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)))
protein
format (file extension .tme
), as generated by the
tptp2X
program.
tptp_before.tme
is 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.tme
is 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
#(onto_file([#(print_proof)], '/tmp/pr1.pl')).after
#(run)
. As a side effect of running the task
a proof term is then printed to the file /tmp/pr1.pl
.
$ proofs_to_dot.pl -tgif -d/tmp /tmp/pr1.pl $ xv /tmp/proof_00001.gif