============================================================================== KRHyper USER MANUAL (Draft) - Release 2005-04-28-09:57 ============================================================================== ============================================================================== Features ============================================================================== - Processing of first order clauses. - Bottom-up incremental ("seminaive") evaluation for proving and model generation. This can be viewed as a refinement of hypertableau in which non-branching nodes are merged. - Processing of disjunctions in hypertableau manner. Models can be enumerated. - Iterative deepening on a term weight limit ensures fairness necessary for refutational completeness. It also softens the "bulk" strategy of seminaive evaluation, especially for refutational tasks which involve construction of nested terms. - Stratified logical operators \+/1 and findall/3. - Indexing configurable per predicate. - Support for ISO-Prolog datatypes: atom (i.e. symbolic constant), compound, integer and float. String is not supported, since its functionality is subsumed by type atom. - Prolog-like builtins for arithmetic and sets as ordered lists. - Generates proofs that can be output as terms and viewed as graphs. ============================================================================== Invocation ============================================================================== krh [-tty] [FILE]... Process the statements in the given files. With no FILE, or when FILE is -, process standard input. If standard input is processed, and it is a terminal, the system prints a prompt whenever it is ready to read a statement. Signal SIGINT (CTRL-C) can be used to abort processing of a proving/ model generation task. In a terminal CTRL-D (end of file) can be used to quit the program. Options: -tty Forces to handle the standard input in terminal mode, also if it is not actually connected to a terminal. ============================================================================== Statements ============================================================================== A statement is either of the form #(Command). which effects that the given command will be executed. Or it is a clause that will be asserted. Statements must be written in canonical ISO-Prolog syntax. Lists may also be written in Prolog list notation, using square brackets and the vertical bar. Strings in double-quotes are not supported. ============================================================================== Concrete Syntax ============================================================================== Statements must be written in canonical ISO-Prolog syntax. Lists may also be written in Prolog list notation, using square brackets and the vertical bar. Strings in double-quotes are not supported. ============================================================================== Syntax of Clauses ============================================================================== In general the syntax is compatible with the syntax of the Protein prover ("tme" format), that can be produced by the TPTP library. Clause ::= Unit | Disjunction | Rule | false Unit ::= Atom Disjunction ::= Disjunction of Atom Rule ::= Head :- Body Head ::= false | Conjuction of Atom | Disjunction of Atom Body ::= true | Conjunction of BodyLiteral BodyLiteral ::= Atom | \+(Atom) | not(Atom) | not_subsumed(Atom) | findall(Absterm, Query, Result) Conjunction of Element ::= Element | (Element, Conjunction of Element) Disjunction of Element ::= (Element; Element) | (Element; Disjunction of Element) The main functor of an atom may not be one of the symbols used as logic operator: :-/2, ;/2 ,/2, true/0, false/0, \+/1, not/1, findall/3, not_subsumed/1. Note: Atom is used here as common in the field of automated deduction for ``atomic formula'', not in the sense of Prolog, where it means a 0-ary function symbol. ============================================================================== Restrictions on Input Formulas ============================================================================== In the hypertableau calculus, the disjuncts of an inferred disjunction may not share variables. The krhyper3 system ensures this for Horn clauses (obviously) and range restricted clauses. For other kinds of input clauses, auxiliary predicates that enumerate the domain can be used. The preprocessor "scripts/pre.pl" performs such a transformation (when necessary) of an arbitrary first order formula. See section "Auxiliary Programs". ============================================================================== Meaning of Logic Operators ============================================================================== The system handles unit and nonunit clauses differently: A unit clause is stored as fact (added to an hypertableau branch). The set of facts with a certain predicate is called the predicate's extent. Disjunctions and rules are kept in a special store. For a proving or model generation task, subsets of them are compiled and used as input clauses (in the sense of input resolution or hypertableau) for inferencing new facts. Note: Disjunctions 'D' and the empty clause 'false' are handled in the same way as rules 'D :- true' or 'false :- true' respectively. A rule 'U :- true' where 'U' is a unit is handled as a rule, i.e. stored in the rule store instead of the fact store. Note: Subsumption within input clauses is currently not supported. The following special logic operators are supported: false 'false' may appear as rule Head to express a clause with only negative literals. It can also appear as Clause, representing the empty clause. true 'true' may appear as rule Body to express a clause with only positive literals. \+(Atom) not(Atom) Stratified negation as failure. Atom is an atom. Each variable in Atom must also appear in an ordinary literal or as output argument of another special literal. Subgoal sorting ensures that at least one such appearance preceedes evaluation of the negative literal. not(Atom) is an alternate syntax for \+(Atom). not_subsumed(Atom) [Experimental] A variation of negation that is intended to express special forward subsumption rules. It is similar to \+/1 except that - it suceeds if there is no fact which is a variant of Atom or more general in the fact base, whereas \+ uses unification. - it does not use stratification, so a failure of not_subsumes(Atom) should only effect that redundant, but not wrong facts are derived. - at subgoal sorting not_subsumed literals are put to the end of the clause (rationale: they should be instantiated as much as possible). findall(Absterm, Query, Result) Stratified set abstraction construct. It is similar to the Prolog's findall/3, except that Result is sorted and contains no duplicates. Absterm is the constructor term of the set elements. Query is an atom. Each variable in Query must also appear in an ordinary literal or as output argument of a another special literal. Subgoal sorting ensures that at least one such appearance preceedes evaluation of the findall literal. A variable in Absterm may not appear in another literal. ============================================================================== Commands ============================================================================== Note: Commands starting with 'print_' produce Prolog readable output. ------------------------------------------------------------------------------ Command: help/0 ------------------------------------------------------------------------------ 'help' prints documentation. ------------------------------------------------------------------------------ Command: run/0 ------------------------------------------------------------------------------ 'run' computes the first model or a refutation. If a model is found, it becomes the current model. ------------------------------------------------------------------------------ Command: run/1 ------------------------------------------------------------------------------ 'run(p/n)' is like run/0, but only the subset of input rules that is relevant for the given predicate is used. ------------------------------------------------------------------------------ Command: next/0 ------------------------------------------------------------------------------ 'next' computes the next model. If a model is found, it becomes the current model. ------------------------------------------------------------------------------ Command: abandon/0 ------------------------------------------------------------------------------ 'abandon' abandons the current model. ------------------------------------------------------------------------------ Command: print_extent/0 ------------------------------------------------------------------------------ 'print_extent' prints the extents of all predicates in the current model. ------------------------------------------------------------------------------ Command: print_extent/1 ------------------------------------------------------------------------------ 'print_extent(p/n)' prints the extent of the predicate p/n in the current model. ------------------------------------------------------------------------------ Command: print_extent_with_proofs/1 ------------------------------------------------------------------------------ 'print_extent_with_proofs(p/n)' prints a Fact-Proof pair for each fact in the extent of the predicate p/n in the current model. [Works not yet with disjunctions]. ------------------------------------------------------------------------------ Command: print_proof/0 ------------------------------------------------------------------------------ 'print_proof' prints the proof if the current result is closed. Output format is the same as of 'print_extent_with_proofs'. [Output for non-Horn problems and open results is still experimental]. ------------------------------------------------------------------------------ Command: print_proof_1/0 ------------------------------------------------------------------------------ 'print_proof_1' prints the proof if the current result is closed. Output format is the same as of 'print_extent_with_proofs'. [Output for non-Horn problems and open results are still experimental]. [Deprecated - old version of print_proof] ------------------------------------------------------------------------------ Command: print_negative_units/0 ------------------------------------------------------------------------------ 'print_negative_units' prints the negative clauses of the current model which are maintained for heuristic purposes, such as complement splitting. ------------------------------------------------------------------------------ Command: print_rules/0 ------------------------------------------------------------------------------ 'print_rules' prints all rules. ------------------------------------------------------------------------------ Command: print_declarations/1 ------------------------------------------------------------------------------ 'print_declarations(p/n)' prints the currently effective declarations for the predicate p/n. ------------------------------------------------------------------------------ Command: print_declarations/0 ------------------------------------------------------------------------------ 'print_declarations' prints the currently effective declarations. ------------------------------------------------------------------------------ Command: print_settings/0 ------------------------------------------------------------------------------ 'print_settings' prints the currently effective flag and parameter settings. ------------------------------------------------------------------------------ Command: print_compiled_rules/0 ------------------------------------------------------------------------------ 'print_compiled_rules' prints all rules after preprocessing, especially body literals are sorted heuristically and obeying builtins. This command may be useful to generate input for other preprocessing operations such as a magic sets transformation. [Currently does not properly print literals with findall/3 and negation operators other than \+/1.] ------------------------------------------------------------------------------ Command: show_symbols/0 ------------------------------------------------------------------------------ 'show_symbols' prints information about symbols in the symbol table. ------------------------------------------------------------------------------ Command: show_predicates/0 ------------------------------------------------------------------------------ 'show_predicates' prints information about predicates with respect to the current model. ------------------------------------------------------------------------------ Command: show_extent_size/1 ------------------------------------------------------------------------------ 'show_extent_size(p/n)' prints information about the extent size of predicate p/n in the current model. ------------------------------------------------------------------------------ Command: show_stratification/0 ------------------------------------------------------------------------------ show_stratification prints information about the stratification of input rules performed by the system. ------------------------------------------------------------------------------ Command: set_flag/2 ------------------------------------------------------------------------------ 'set_flag(Flag, Boolean)' assigns the given truth value to the flag. The boolean can be specified as 'true'/'false' or 'on'/'off'. ------------------------------------------------------------------------------ Command: set_parameter/2 ------------------------------------------------------------------------------ 'set_parameter(Parameter, Integer)' assigns the given integer value to the parameter. ------------------------------------------------------------------------------ Command: index/2 ------------------------------------------------------------------------------ 'index(p/n, [type=Type, args=Args])' declares an index for the predicate p/n. Type is one of 'none', 'alist_dt' or 'hash_dt'. Args is either 'all' (index on the whole term), an integer n (index on the nth argument) or a list of integers (index on a subterm composed of the respective arguments in the given ordering). ------------------------------------------------------------------------------ Command: discrimination_hints/2 ------------------------------------------------------------------------------ 'discrimination_hints(p/n, Hints)' declares Hints as discrimination hints for the predicate p/n. Hints is a list of floats between 0.0 and 1.0 and has length n. ------------------------------------------------------------------------------ Command: mode/1 ------------------------------------------------------------------------------ 'mode(Template)' declares the ``mode'' of a predicate. It is used for body literal ordering. 'Template' is a term with functor and arity of the predicate. The arguments are 'f', which means that the respective argument can have nonground values in facts with that predicate, or 'b', which means that it has always ground values. By default a mode that assigns 'b' to all argument positions is assumed. Note that, unless builtins are used, mode declarations play only a heuristic role. The effect of different mode declarations for a predicate is undefined. ------------------------------------------------------------------------------ Command: begin_shared_input/0 ------------------------------------------------------------------------------ 'begin_shared_input' enables sharing of subsequent input terms. Input terms are only shared within dynamic begin_shared_input/ end_shared_input contexts. The behavior for nested begin_shared_input/end_shared_input contexts is undefined. ------------------------------------------------------------------------------ Command: end_shared_input/0 ------------------------------------------------------------------------------ 'end_shared_input' disables sharing of subsequent input terms and frees resources used for sharing. ------------------------------------------------------------------------------ Command: abolish/1 ------------------------------------------------------------------------------ 'abolish(p/n)' abolishes predicate p/n. This means its extent and its declarations are removed. ------------------------------------------------------------------------------ Command: clear_rules/0 ------------------------------------------------------------------------------ 'clear_rules' removes all rules. ------------------------------------------------------------------------------ Command: load/1 ------------------------------------------------------------------------------ 'load(Filename)' processes the statements in the specified file. Filename can be a relative pathname. If the load command is called from an input file, the pathname is resolved using the directory of that file. If load is called from standard input, the pathname is resolved relative to the current working directory. ------------------------------------------------------------------------------ Command: load_shell_output/1 ------------------------------------------------------------------------------ 'load_shell_output(ShellCommand)' runs the given shell command in parallel with the krh program. The standard output of the shell command is processed as input by krh. The shell command is interpreted by /bin/sh. Example: #(load_shell_command('canonicalize.pl myfile.tme')) ------------------------------------------------------------------------------ Command: onto_file/2 ------------------------------------------------------------------------------ 'onto_file(StatementList, Filename)' subsequently processes each Statement in StatementList with redirecting standard output to the specified file. ------------------------------------------------------------------------------ Command: progn/1 ------------------------------------------------------------------------------ 'progn(StatementList)' subsequently processes each statement in the list. ------------------------------------------------------------------------------ Command: do_models/1 ------------------------------------------------------------------------------ 'do_models(StatementList)' processes the statements in StatementList like progn but for each model that is found. During processing of the statements, the current model is set to the respective model. ------------------------------------------------------------------------------ Command: write/1 ------------------------------------------------------------------------------ 'write(String)' writes the content of the given string to the standard output (similar to write/1 in Prolog). String is a Prolog-syntax atom. Special sequences, starting with the tilde (~), are interpreted as formatting actions: ~~ Output the tilde itself. ~m Output the number of the current model. ~z Flush the output stream. ------------------------------------------------------------------------------ Command: assert/1 ------------------------------------------------------------------------------ 'assert(Statement)' processes Statement. ------------------------------------------------------------------------------ Command: time/1 ------------------------------------------------------------------------------ 'time(StatementList)' subsequently processes each Statement in StatementList and prints information about the execution time. ------------------------------------------------------------------------------ Command: set_verbosity/1 ------------------------------------------------------------------------------ 'set_verbosity(Integer)' assigns a verbosity value, that determines which messages are printed. It should range from -1 (no messages) to 3 (maximum messages). ------------------------------------------------------------------------------ Command: set_message_output/1 ------------------------------------------------------------------------------ 'set_message_output(OutputStream)' determines the output stream on which messages are printed. By default messages are printed to the standard error stream. Since standard error and standard output use different buffers internally, they are not synchronized. OutputStream can be 'stdout' or 'stderr'. ------------------------------------------------------------------------------ Command: clear_builtins/0 ------------------------------------------------------------------------------ 'clear_builtins' disables builtin predicates, arithmetic evaluation and logic operators with exception of: :-/2, ','/2, ';'/2, 'false'/0. It must be called before any facts or rules are read in. ------------------------------------------------------------------------------ Command: sys_gc/0 ------------------------------------------------------------------------------ 'sys_gv' forces an OCaml garbage collection. ------------------------------------------------------------------------------ Command: sys_print_stat/0 ------------------------------------------------------------------------------ 'sys_print_stat' prints some OCaml system statistics. See documentation of Gc.print_stat in the OCaml standard library for more information. ------------------------------------------------------------------------------ Command: man/1 ------------------------------------------------------------------------------ 'man(Section)' prints the specified section of the documentation. Currently the sections 'general', 'commands', 'flags' and 'parameters' are supported. ------------------------------------------------------------------------------ Command: print_version/0 ------------------------------------------------------------------------------ 'print_version' prints a fact version(Version) with Version an atom indicating the version of krh. ------------------------------------------------------------------------------ Command: exit/0 ------------------------------------------------------------------------------ 'exit' terminates krh with status code 0. ============================================================================== Flags ============================================================================== ------------------------------------------------------------------------------ Flag: back_subsumption, default: false ------------------------------------------------------------------------------ Use back subsumption - i.e. remove derived or input facts if they are subsumed by a newly derived clause. [Works not with disjunctions] ------------------------------------------------------------------------------ Flag: back_subsumption_within_news, default: false ------------------------------------------------------------------------------ Use back subsumption within the set of newly derived clauses. ------------------------------------------------------------------------------ Flag: sort_heads, default: true ------------------------------------------------------------------------------ Sort disjunctive heads heuristically. ------------------------------------------------------------------------------ Flag: check_disjunctions_are_ground, default: true ------------------------------------------------------------------------------ Verify at runtime for each derived disjunction that is it ground. ------------------------------------------------------------------------------ Flag: negative_units, default: true ------------------------------------------------------------------------------ Maintain negative units to detect refutations sooner and enable complement splitting. ------------------------------------------------------------------------------ Flag: merge_inf_input, default: false ------------------------------------------------------------------------------ Merge facts inferred before any disjunctive branching into the input facts. These derived facts then serve as lemmas in subsequent tasks. This flag can be switched on and off around a call to 'run' to generate certain lemmas. ------------------------------------------------------------------------------ Flag: wp_semantics, default: false ------------------------------------------------------------------------------ [Experimental] Enforce the `weak perfect' KRHyper semantics of disjunctions. Overrides effects of other flags conflicting with that semantics. ------------------------------------------------------------------------------ Flag: proof_terms, default: false ------------------------------------------------------------------------------ Generate proof terms for derived facts. ------------------------------------------------------------------------------ Flag: level_cut, default: true ------------------------------------------------------------------------------ Apply the level cut reduction. This is only effective if proof_terms is also set. Note: No level cut is applied at a node whose proof involves stratified negation as failure or findall. ------------------------------------------------------------------------------ Flag: echo, default: false ------------------------------------------------------------------------------ Print each input statement before it is processed. ------------------------------------------------------------------------------ Flag: debug, default: false ------------------------------------------------------------------------------ Debug mode. Print extra information about clause compilation. ------------------------------------------------------------------------------ Flag: show_derived_literals, default: false ------------------------------------------------------------------------------ Show facts as they are derived. May be useful for debugging. Output are Prolog readable statements, one per line: derived_fact(Fact). -- Fact has been derived in an extension step. attached_disjunction(DisjunctionId). -- The tableau has been extended with a disjunction. selected_disjunct(Fact, DisjunctionId). -- Fact has been selected from an attached disjunction. Notes: DisjunctionIds are currently not implemented. Negative facts (see flag negative_units) are currently not considered. ============================================================================== Parameters ============================================================================== ------------------------------------------------------------------------------ Parameter: max_weight_initial, default: 20 ------------------------------------------------------------------------------ The initial weight limit for inferred literals. If -1, weight handling is not used. For infinite Herbrand domains, weight handling can be required to ensure refutational completeness and `finite-branch-model' completeness. ------------------------------------------------------------------------------ Parameter: max_weight_increment, default: 1 ------------------------------------------------------------------------------ The minimum amount by which the weight limit for inferred literals is increased in a weight reset step. If max_weight_increment >= 0, then the actual number used is the maximum of this number and the smallest number by which an additional literal can possibly be inferred. If max_weight_increment = -1, max_weight_initial is used as weight limit and not incremented, yielding an obviously incomplete calculus. ------------------------------------------------------------------------------ Parameter: body_sorting_method, default: 0 ------------------------------------------------------------------------------ Determines the heuristics for sorting body literals. The following values can be used: 0 - A heuristics that ensures permissibility for builtins is used. 1 - The literal order of the input is used, except that delta predicates are preferred. This may be useful on inputs resulting from program transformations. 2 - The literal order of the input is used. ------------------------------------------------------------------------------ Parameter: weighing_method, default: 0 ------------------------------------------------------------------------------ Determines how the weight of a term is computed. The following values can be used: 0 - The size of the term, i.e. the number of occurences of predicate, function and constant symbols as well as variables in it is used. 1 - The depth of the term is used. ============================================================================== Builtins ============================================================================== In these predicate signatures specifications + indicates an input argument, - indicates an output argument. Each variable in an input argument must also appear in an ordinary literal or as output argument of another special literal. Subgoal sorting ensures that at least one such appearance preceedes evaluation of the builtin literal. Of course an output argument may be also be bound at evaluation of a builtin. Arithmetics The semantics of these builtins is as specified for ISO-Prolog, is(-,+) <(+,+) =:=(+,+) =<(+,+) =\=(+,+) >(+,+) >=(+,+) Sets Represented as Ordered Lists The semantics of these builtins is the same as in the Ordset Prolog library, however input arguments must be bound to ground terms. sort/2 ord_insert(+,+,-) ord_intersection(+,+,-) ord_subtract(+,+,-) ord_symdiff(+,+,-) ord_union(+,+,-) ord_subset(+,+) ord_disjoint(+,+) ord_intersect(+,+) Lists append(+,+,-) List concatenation, as by the Prolog predicate append/3, however only the mode append(+,+,-) is supported. The first argument must be bound to a list of ground terms. ============================================================================== Evaluables ============================================================================== The following arithmetic evaluables are currently implemented with the semantics according to ISO-Prolog. */2 +/2 -/1 -/2 //2 abs/1 float/1 truncate/1 ============================================================================== Indexing ============================================================================== index(p/n, [type=Type, args=Args]) This command declares an index for the predicate p/n. Multiple indices can be declared for a predicate. Type determines the kind of index. It can be: none No indexing is performed. alist_dt Discrimination tree indexing using association lists for functor dispatch. hash_dt Discrimination tree indexing using hash tables for functor dispatch. Args determines the arguments used by the index. It can be: all Index on the whole term. An integer n Index on the nth argument (starting from 0). A list of integers. Index on a subterm composed of the respective arguments in the given ordering. The default index is [type=alist_dt, args=all]. Notes: - The default index performs poor if the first arguments are not instantiated. - EDB predicates (i.e. predicates not appearing in a clause head) are not written during processing, so many indexes on them are not time expensive. - An index on a variable that is not shared with another literal can not be used. - For IDB predicates (i.e. predicates appearing in a clause head) it may be good to have an index on "all" arguments, (such as the default index) since it is useful for subsumption of newly derived facts. - htable_dt may be useful if many different constants or functors appear in an argument. ============================================================================== Discrimination Value Hints ============================================================================== So called "discrimination values" may be used as hints for optimization: A discrimination value is associated with an argument position of a predicate. It is a float ranging between 0.0 and 1.0. It estimates for that argument position the number of different argument values divided by the extent size of the predicate. So, as extremes, an argument corresonding to a key attribute has a discrimination value of 1.0. An argument which has the same value for the whole predicate has a discrimination value of 0.0. By default arguments in lower positions receive a higher discrimination value than those in higher positions. The leftmost argument receives a value of 0.5. Discrimination hints may be specified with the following command: #(discrimination_hints(p/n, Hints)) where Hints is a list of discrimination values with length n. ============================================================================== Limits ============================================================================== The maximal number of distinct variables in a clause is determined when the system is compiled. By default it is 64. =========================================================================== Auxiliary Programs ============================================================================== The following auxiliary programs can be found in krh/scripts: pre.pl [-rr] FILE Preprocessor. Reads a "tme" file with first order clauses, and writes the transformed clauses to the standard output. Output is written in canonical form, such that it can be input to krh directly. The following transformations are performed: - If the clause set contains a non-Horn clause and is not range restricted, domain construction clauses and literals are added, to make them suitable as input for krh. Options: -rr If this flag is set, the input is transformed to a range restricted clause set. Operator settings for inputs are as in SWI-Prolog with addition of op(500,fx,#). canonicalize.pl FILE Reads a prolog file and writes it in canonical form to stdout. Operator settings for inputs are as in SWI-Prolog with addition of op(500,fx,#). canfilter.pl Reads prolog terms and writes them canonically to standard output. This can be piped before krh to allow noncanonical input, e.g: canfilter.pl | krh -tty myconfig.tme - Operator settings for inputs are as in SWI-Prolog with addition of op(500,fx,#). pp.pl [-init=INITFILE] [FILE] Reads FILE which is in prolog syntax (default stdin) and pretty prints it to stdout. If the option -init=INITFILE is present, consult(INITFILE) is called before FILE is read. INITFILE can for example contain custom operator declarations. proofs_to_dot.pl [-tTYPE] [-dDIR] FILE Converts proofs to graphs in dot format or to gif image files. FILE contains Prolog readable Goal-Proof statements. For each statement a graph file is written in directory DIR (default /tmp). Depending on the format a dot file (TYPE dot, default) or a gif image (TYPE gif) is written. Filenames are of the form proof_NNNNN.dot or proof_NNNNN.gif, where NNNNN is a zero padded number, starting from 1. [Output for non-Horn proofs is preliminary] gen-doc-html.sh Generates HTML documentation about the implementation with ocamldoc. The sources are expected to be in $KRHDIR/src. Output is written to $KRHDIR/generated_doc. $KRHDIR defaults to $HOME/krh. gen-dot.sh Generates images showing module dependencies of the implementation with ocamldoc. The sources are expected to be in $KRHDIR/src. Output is written to $KRHDIR/generated_doc. $KRHDIR defaults to $HOME/krh.