Usage Hints

Contents

Input Syntax: Canonical Prolog

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 -
    

First Order Disjunctions: Preprocessor

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.

Using KRH within Emacs

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)))
    

Examples

Testing a TPTP Problem

Enumerating Models

Viewing the Proof Graph of a Refutation