============================================================================== E-KRHyper USER MANUAL (Draft) - Release 2007-11-19 ============================================================================== ============================================================================== 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. $$atleast(Cardinality, X, Y, SkolemTerms, PosFacts, NegFacts) (alternative short form: $$atleast(Cardinality, X, Y, PosFacts, NegFacts)) A Description-Logics-oriented cardinality operator. This may occur as a predicate both in head and body literals of clauses. Cardinality must be an integer. X must be a variable. Y must be a variable not occurring in any other literal of the clause. SkolemTerms must be a list [C1,...,Cs] of logical term, with s = Cardinality. PosFacts and NegFacts must be lists (using brackets: [PF1,...,PFm], [NF1,...,NFn]) of logical atoms. Once an $$atleast-literal is derived into the tableau, each element of the SkolemTerms C1,...,Cs will be regarded as an individual, and for every such individual Ci the atoms given in PosFacts and NegFacts will be asserted into the tableau as facts. This means that for each Ci, the facts PF1i,...,PFmi are asserted into the tableau, with PF1i,...,PFmi being created from PF1,...,PFm by substituting every occurrence of Y with Ci. Also, for each Ci, the negative clauses 'false :- NF1i.',...,'false :- NFni.' are asserted, with NF1i,...,NFni being created from NF1,...,NFn by substituting every occurrence of Y with Ci. Also, inequality clauses of the form 'false :- Ck=Cl.' are added for all pairs out of SkolemTerms. The short form notation using '$$atleast/5' omits the SkolemTerms argument. Any atom using this notation is automatically transformed into the full '$$atleast/6' notation, with SkolemTerms being generated by applying Cardinality-amount of fresh Skolem functions to X. The evaluation of $$atleast-literals can be deactivated with the clear_builtins command. If the evaluation of $$atleast-literals is not deactivated and $$atleast-literals are present in the current clause set, then E-KRHyper automatically runs in E-Hyper mode with builtin equality evaluation.============================================================================== Commands ============================================================================== Note: Commands starting with 'print_' produce Prolog readable output. ------------------------------------------------------------------------------ Command: automatic_max_weight_initial/0 ------------------------------------------------------------------------------ The initial maximum literal weight will be determined automatically using heuristics. Any manual setting of the parameter 'max_weight_initial' will be ignored, unless it is -1, in which case no weight handling is used. ------------------------------------------------------------------------------ Command: continue_tableau/0 ------------------------------------------------------------------------------ Continues a (possibly interrupted) tableau. ------------------------------------------------------------------------------ Command: change_clause_set/1 ------------------------------------------------------------------------------ 'change_clause_set()' switches the current work environment to a clause set named . The current clause set is saved and removed from the tableau computation. Instead the set is loaded. If no set named exists yet, it will be created, and it will be empty. Any clauses added after this will be added to the set . A saved clause set can be reloaded by using this command with the saved set's name. The initial default clause set has the name 'default'. ------------------------------------------------------------------------------ Command: delete_clause_set/1 ------------------------------------------------------------------------------ 'delete_clause_set()' deletes the clause set named . If is the current clause set, then the prover will also switch to the 'default' clause set. If is 'default', the default clause set will be replaced by an empty clause set. ------------------------------------------------------------------------------ Command: save_clause_set_to_file/1 ------------------------------------------------------------------------------ 'save_clause_set_to_file()' saves the current clause set into a file named . If such a file exists, it will be overwritten without warning. The saved file will be binary and contain all indexing information. This means that loading this file at a later date will not require re-indexing the clauses, so for large clause sets this method is faster than reloading the clauses in their original TPTP or TME format. ------------------------------------------------------------------------------ Command: load_clause_set_from_file/1 ------------------------------------------------------------------------------ 'load_clause_set_from_file()' saves the current clause set like 'change_clause_set' does, and loads a clause set from the file instead. This file must be a binary file created by 'save_clause_set_to_file'. ------------------------------------------------------------------------------ Command: deactivate_automatic_max_weight_initial/0 ------------------------------------------------------------------------------ Undoes the effect of 'automatic_max_weight_initial'. ------------------------------------------------------------------------------ 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: compute_answer_for_tptp_fof_variable/1 ------------------------------------------------------------------------------ 'compute_answer_for_tptp_fof_variable('')' makes E-KRHyper store the bindings for the variable during the derivation process. For this to have any effect, the variable must occur in a tptp first order conjecture. Once a tableau refutation has been found, the binding(s) can be listed using the command 'print_answer_units'. A number of '$answer'/1-units will be listed, each having as its argument one term that was bound to . Only one variable can be treated this way, as this command causes the transformation of input clauses. The command must be given before the TPTP-conjecture is read. The negation of TPTP-conjectures must be enabled (this is the case by default). The command is a combination of the commands 'set_tptp_fof_answer_variable' and 'set_flag(tptp_fof_compute_answer_predicate, true)'. ------------------------------------------------------------------------------ Command: webservices_interface/1 ------------------------------------------------------------------------------ 'webservices_interface_socket(, )' tells E-KRHyper to use the external webservices interface specified by the string and the integer for processing webservice query literals ($$wsq/3). If no interface is specified using this command, then the interface will be assumed to run on the same machine as E-KRHyper (127.0.0.1) on port 64000. Only one interface can be used. If this command is issued multiple times with different addresses, then the last one will be used during the proof derivation. ------------------------------------------------------------------------------ Command: save_input_state/0 ------------------------------------------------------------------------------ 'save_input_state' saves the current state of the set input clauses. If further input clauses are added after this, the set of input clauses can be rolled back to the saved state using 'load_previous_input_state'. Multiple states can be saved consecutively. Multiple 'load_previous_input_state'- commands can then be used to iterate through the saved states in reverse order. ------------------------------------------------------------------------------ Command: load_previous_input_state/0 ------------------------------------------------------------------------------ 'load_previous_input_state' returns the set of input clauses to the state saved by the most recent 'save_input_state'-command. Multiple 'previous_input_state'-commands can then be used to iterate through the saved states in reverse order. The command has no effect if no state has been saved yet. ------------------------------------------------------------------------------ Command: load_partition/1 ------------------------------------------------------------------------------ 'load_partition()' loads a partitioning file named and performs the partitioning assignments included. A partitioning file may also include further occurrences of load_partition/1. ------------------------------------------------------------------------------ Command: szs_problem_name/1 ------------------------------------------------------------------------------ 'szs_problem_name/1' enters the problem name required for SZS-conforming output. ------------------------------------------------------------------------------ Command: print_current_subterm_table_keys/0 ------------------------------------------------------------------------------ Debugging function, prints the keys of the current subterm_table. ------------------------------------------------------------------------------ Command: print_last_max_weight_used/0 ------------------------------------------------------------------------------ Print the tem weight limit last in use. ------------------------------------------------------------------------------ Command: print_current_compiled_rules/0 ------------------------------------------------------------------------------ 'print_current_compiled_rules' prints the set of compiled rules in the current model. ------------------------------------------------------------------------------ Command: print_current_clauses_contain_impure_vars/0 ------------------------------------------------------------------------------ 'print_current_clauses_contain_impure_vars' prints 'Impure variables: yes.' if at least one current clause contains at least one variable shared between head literals and not found in the body, and 'Impure variables: no.' otherwise. ------------------------------------------------------------------------------ Command: print_current_equation_units/0 ------------------------------------------------------------------------------ 'print_current_equation_units' prints the set of equation units in the current model. ------------------------------------------------------------------------------ Command: begin_selected_input/1 ------------------------------------------------------------------------------ 'begin_selected_input([method=Method, queries=Queries, tolerance=Tolerance, persistent=Persistent])': Logical input read after this command is subject to a selection heuristic. Only clauses and formulas selected by the heuristic will actually be used during reasoning. The actual selection will be carried out once the command 'end_selected_input' is executed. The selection heuristic will evaluate the logical input entered between these commands, and only the selected clauses and formulas will be entered into the actual reasoning environment. (Before 'end_selected_input', none of the entered input will show up when using the print-commands.) Input entered outside a 'begin_selected_input'/'end_selected_input' pair is treated as normal input and not subject to any selection. If multiple calls are made to 'begin_selected_input' before any 'end_selected_input' is executed, only the last specified selection heuristic will be applied. The parameters are optional, default values (see below) will be used for non-specified parameters. The Method parameter must be one of: - 'none': no special selection algorithm, all input is used, - 'sine': Krystof Hoder's Sine/SInE selection algorithm, - 'ekrh': an experimental version based on the Sine selection. Default: 'none'. The Queries parameter must be one of: - 'cq': use TPTP-FOF 'conjecture' and 'question' type formulas to select, - 'cqn': like 'cq', but also use all negative clauses. Default: 'cq'. The Tolerance parameter must be an integer or float value. Default: 1. The Persistent parameter must be one of: - 'true': the full input will be kept after selection to enable further selections, however, only the selected input is used for reasoning, - 'false': any non-selected input is completely discarded. Default: 'false'. ------------------------------------------------------------------------------ Command: end_selected_input/0 ------------------------------------------------------------------------------ See 'begin_selected_input'. ------------------------------------------------------------------------------ Command: end_persistent_selected_input/0 ------------------------------------------------------------------------------ This command can be set after 'begin_selected_input' as an alternative to 'end_selected_input'. Any input between 'begin_selected_input' and 'end_persistent_selected_input' will be treated as a static ontology. This means that this command will compute the dependencies within the enclosed persistent input, but it will not perform The actual selection will be done when 'select_from_input' is called, and it will be based on all input enclosed between 'begin_nonpersistent_queries' and 'end_nonpersistent_queries'. As the name of this command implies, the input is treated as persistent. This input remains within the system over repeated loading and saving of states. As such it is possible to enter an ontology and compute its dependencies once using this command, then add some queries and perform the selection with 'select_input', then get back to the state before the selection via 'load_previous_input_state', enter new queries (the old one having been discarded) and perfom a new selection from the persistent input with the new queries. ------------------------------------------------------------------------------ Command: begin_nonpersistent_queries/0 ------------------------------------------------------------------------------ This command works in conjunction with a subsequent call to 'end_nonpersistent_queries'. Any input enclosed between these commands will be treated as queries for the purpose of the heuristic selection (see 'begin_selected_input'), that is, their symbols will select clauses from the other input (the ontology). The input enclosed between these commands will always participate in the reasoning, even if any of its clauses or formulas was not marked as a 'conjecture' or 'question' in TPTP syntax. The input is also non-persistent in that if a state from before entering the input is loaded (see 'load_previous_input_state'), then this input is discarded. ------------------------------------------------------------------------------ Command: end_nonpersistent_queries/0 ------------------------------------------------------------------------------ See 'begin_nonpersistent_queries'. Input after this command is treated normally, it is not subject to any selection and will participate in the reasoning. Note that the heuristic selection using the non-persistent queries must be started explicitly using 'select_from_input'. ------------------------------------------------------------------------------ Command: select_from_input/0 ------------------------------------------------------------------------------ This command triggers a heuristic selection of clauses from the input. Only the selected clauses will participate in the reasoning process. The input must have been prepared with 'begin_selected_input'. ------------------------------------------------------------------------------ Command: select_from_input_alg/1 ------------------------------------------------------------------------------ 'select_from_input_alg([method=Method])': Like 'select_from_input', but allows specifiying a selection algorithm in a manner similar to 'begin_selected_input'. Note that the input must have been entered and prepared with 'begin_selected_input'. The specifications entered here may override those stated with 'begin_selected_input' to a degree: If the input was prepared for 'method=all', then only 'method=all' will work here. If the input was prepared for 'method=sine' or 'method=ekrh', then 'method=all', 'method=sine' and 'method=ekrh' will work here. ------------------------------------------------------------------------------ Command: print_answer_units/0 ------------------------------------------------------------------------------ 'print_answer_units' prints the set of answer predicate units that have been computed so far. If a proof has been found, but no answer variable has been instantiated, then an unspecific '$answer.' will be given. ------------------------------------------------------------------------------ Command: print_partial_answer_units/0 ------------------------------------------------------------------------------ 'print_partial_answer_units' prints the set of partial answer predicate units that have been computed so far. A partial answer unit takes the form '$partial_answer'(, , ). where is a Prolog-style list of those literals from a conjecture based clause that unified with the current extent (displayed using the original variable names), and where is a Prolog-style list of special terms that express the substitution used for the unification. Each such binding term takes the form '$bound_to'(, ), where is a variable occuring in and is the term substituting the . is a list of those literals that were not unified, in the order used by E-KRHyper. The first literal in this list is thus the literal that failed to unify, while the remaining elements were never tested. ------------------------------------------------------------------------------ Command: print_extent/0 ------------------------------------------------------------------------------ 'print_extent' prints the extents of all predicates in the current model. ------------------------------------------------------------------------------ Command: print_lemmas/0 ------------------------------------------------------------------------------ EXPERIMENTAL! 'print_lemmas' prints the subset the extent that has been computed before the first split and which thus holds in all tableau branches (although some units may be subsumed in some branches). ------------------------------------------------------------------------------ Command: print_tptp_fof_lemma/0 ------------------------------------------------------------------------------ EXPERIMENTAL! 'print_tptp_fof_lemma' is essentially the same as 'print_lemmas', but the output is printed as a single first-order axiom in the TPTP format. ------------------------------------------------------------------------------ Command: save_lemmas/0 ------------------------------------------------------------------------------ Saves lemmas for future use. Previously saved lemmas will be overwritten. ------------------------------------------------------------------------------ Command: clear_lemmas/0 ------------------------------------------------------------------------------ Clears all saved lemmas. ------------------------------------------------------------------------------ Command: insert_lemmas/0 ------------------------------------------------------------------------------ Inserts all saved lemmas into the input. ------------------------------------------------------------------------------ Command: print_closing_lemmas/0 ------------------------------------------------------------------------------ 'print_closing_lemmas' prints any closing lemmas that have been learnt in the previous derivation by setting the 'learn_closing_lemmas' flag. ------------------------------------------------------------------------------ Command: print_tptp_closing_lemmas/0 ------------------------------------------------------------------------------ Like 'print_closing_lemmas', but uses TPTP output syntax. ------------------------------------------------------------------------------ Command: add_closing_lemmas_to_input/0 ------------------------------------------------------------------------------ 'add_closing_lemmas_to_input' adds any closing lemmas that have been learnt in the previous derivation (by setting the 'learn_closing_lemmas' flag) to the normal input clauses. ------------------------------------------------------------------------------ Command: clear_closing_lemmas/0 ------------------------------------------------------------------------------ 'clear_closing_lemmas' deletes any closing lemmas that have been learnt in the previous derivation by setting the 'learn_closing_lemmas' flag. Note that closing lemmas that have been turned into input clauses via the 'add_closing_lemmas_to_input' command are not deleted. ------------------------------------------------------------------------------ Command: print_model/0 ------------------------------------------------------------------------------ 'print_model' prints the current model, which means all positive unit clauses in the current branch. ------------------------------------------------------------------------------ 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_clauses/0 ------------------------------------------------------------------------------ 'print_proof_clauses' prints the input clauses and facts required for the proof if the current result is closed. ------------------------------------------------------------------------------ Command: print_szs_proof/0 ------------------------------------------------------------------------------ 'print_szs_proof' prints the proof if the current result is closed. Output format is similar to that of 'print_proof', except that extra control clauses are added to make the output suitable for the 'post_szs.pl' postprocessor. [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: set_tptp_fof_answer_variable/1 ------------------------------------------------------------------------------ 'set_tptp_fof_answer_variable(s)' declares the variable with the name 's' to be the answer variable used for the computation of the '$answer'-predicate units. See 'tptp_fof_compute_answer_predicate'. The string argument for the variable name must be given in single quotes. The variable name must be set before the tptp formula input is read. The default name of the answer variable is 'FOCUS'. ------------------------------------------------------------------------------ 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: set_max_model_size_for_preds/3 ------------------------------------------------------------------------------ 'set_max_model_size_for_preds(Predicates, Integer, Type)', with Predicates being a list of predicate specifications of the form p/n (name/arity), and Integer being an integer number. Type must be one of the strings specified below. This command ensures that the computation of a branch will be closed as soon as its number of units with predicates from the Predicates list reaches Integer. Type specifies which kind of units count towards the limit: - 'all': all units of the listed predicates count, - 'skolem': only units containing Skolem terms (and a listed predicate) count. Only one restriction defined by this command is observed during reasoning, i.e. using this command several times with different values will not cause E-KRHyper to observe all of these restrictions; instead the prover will only observe the most recently defined restriction. Set Integer to -1 to disable any previously made restriction. When disabling in this way, the value for Predicates is irrelevant, and it may be the empty list. ------------------------------------------------------------------------------ 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: clear_builtin/1 ------------------------------------------------------------------------------ 'clear_builtin(s/n)' removes any special evaluation of the builtin/evaluable function or predicate symbol 's' with arity n. ------------------------------------------------------------------------------ Command: abolish/1 ------------------------------------------------------------------------------ 'abolish(p/n)' abolishes predicate p/n. This means its extent and its declarations are removed. ------------------------------------------------------------------------------ Command: compute_partitions/0 ------------------------------------------------------------------------------ Uses E-KRHypers builtin partition computation. ------------------------------------------------------------------------------ Command: assign_filename_to_predicate/2 ------------------------------------------------------------------------------ Used for knowledge-base partitioning. 'assign_filename_to_predicate(Filename, P/A)' declares that the file named Filename contains partitioning information for predicate P with arity A. If partitioning information is required for this predicate, then all files assigned to it will be loaded. Multiple commands can be used to assign multiple filenames. ------------------------------------------------------------------------------ Command: assign_clause_to_predicate/2 ------------------------------------------------------------------------------ Used for knowledge-base partitioning. 'assign_clause_to_predicate(Clause, P/A)' declares that Clause may be required for the computation of predicate P with arity A. Clause must be an input clause that has already been given to E-KRHyper; this command cannot be used to enter input clauses, only to assign a special status to already entered clauses. A clause can be assigned to multiple predicates by applying this command for each predicate. This command is an experimental preprocessing-step. It may be computationally intensive when many clauses have been entered into the system. ------------------------------------------------------------------------------ Command: activate_partitioning/0 ------------------------------------------------------------------------------ When partitioning is activated, upon '#(run)' or '#(run_relevant)' all clauses which cannot be used to derive a refutation for any current query clause will be removed from that run. This behaviour can be undone with 'deactivate_partitioning'. ------------------------------------------------------------------------------ Command: activate_current_partitions/0 ------------------------------------------------------------------------------ Irrelevant clauses will be deactivated in the same manner as triggered by '#(activate_partitioning)', but without actually setting this as a standard behaviour for each run, and without performing a run. This is mostly intended for debugging and monitoring the partitioning algorithm. The clauses are brought back again with '#(deactivate_partitioning)'. ------------------------------------------------------------------------------ Command: print_partition_statistics/0 ------------------------------------------------------------------------------ Prints debugging information about the currently active partition. ------------------------------------------------------------------------------ Command: deactivate_partitioning/0 ------------------------------------------------------------------------------ 'deactiviate_partitioning' returns clauses back to the reasoning which have been removed with 'activate_partitioning'. ------------------------------------------------------------------------------ Command: add_equality_axioms/0 ------------------------------------------------------------------------------ Adds equality axioms with respect to the current input. ------------------------------------------------------------------------------ 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', 'stderr' or a filename. ------------------------------------------------------------------------------ Command: streamcom/0 ------------------------------------------------------------------------------ 'streamcom' ------------------------------------------------------------------------------ Command: start_virtual_timer/1 ------------------------------------------------------------------------------ 'start_virtual_timer(Seconds)' starts a virtual timer, which will terminate E-KRHyper after seconds. ------------------------------------------------------------------------------ Command: start_wallclock_timer/1 ------------------------------------------------------------------------------ 'start_wallclock_timer(Seconds)' starts a wallclock timer, which will terminate E-KRHyper after seconds. ------------------------------------------------------------------------------ Command: stop_virtual_timer/0 ------------------------------------------------------------------------------ 'stop_virtual_timer' stops the virtual timer. ------------------------------------------------------------------------------ Command: stop_wallclock_timer/0 ------------------------------------------------------------------------------ 'stop_wallclock_timer' stops the wallclock timer. ------------------------------------------------------------------------------ Command: set_memory_limit/1 ------------------------------------------------------------------------------ 'set_memory_limit(MB)' sets a memory limit to the given number of MB. E-KRHyper will terminate when this limit is reached. There is no limit set by default. Once a limit is set, it can be switched off again by 'set_memory_limit(-1)'. ------------------------------------------------------------------------------ Command: use_path_variable/1 ------------------------------------------------------------------------------ 'use_path_variable()': when processing include-directives, the prover will look for the included files relative to the value of the environment variable . ------------------------------------------------------------------------------ Command: ignore_file/1 ------------------------------------------------------------------------------ 'ignore_file()': the file will not be loaded, even if it is requested by an include-directive. If is a relative filename, the path given in the path variable (see 'use_path_variable') will be used to obtain a complete path for this file. If there is no path prefix stored in the path variable, then E-KRHyper will assume to refer to a file in the current directory. ------------------------------------------------------------------------------ Command: clear_builtins/0 ------------------------------------------------------------------------------ 'clear_builtins' disables builtin predicates, arithmetic evaluation and logic operators with exception of: :-/2, ','/2, ';'/2, 'false'/0, and 'true'/0. It must be called before any facts or rules are read in. ------------------------------------------------------------------------------ Command: clear_limit_block/0 ------------------------------------------------------------------------------ 'clear_limit_block' deactivates a command block induced by an exceeded timeout or memory limit. See flag 'limit_block'. ------------------------------------------------------------------------------ Command: sys_gc/0 ------------------------------------------------------------------------------ 'sys_gc' 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 ekrh. ------------------------------------------------------------------------------ Command: exit_if_finished/0 ------------------------------------------------------------------------------ 'exit_if_finished' terminates ekrh with status code 0 if the last run resulted in a proof or a model. ------------------------------------------------------------------------------ Command: exit/0 ------------------------------------------------------------------------------ 'exit' terminates ekrh with status code 0. ============================================================================== Flags ============================================================================== ------------------------------------------------------------------------------ Flag: atleast_successors_as_dois, default: false ------------------------------------------------------------------------------ Treat the successor individuals created by the $atleast rules as distinct object identifiers (DOIs). As DOIs are automatically subject to the integrated unique name assumption, the $atleast rule no longer needs to create inequalities that keep the successors pairwise distinct. ------------------------------------------------------------------------------ Flag: use_given_clause_algorithm, default: false ------------------------------------------------------------------------------ Use the Given Clause Algorithm instead of the default Semi-Naive Evaluation. ------------------------------------------------------------------------------ Flag: passive_input, default: false ------------------------------------------------------------------------------ If true, input formulas and clauses will be treated as passive when using the Given Clause Algorithm, otherwise as active. This flag has no effect when 'use_given_clause_algorithm' is false. ------------------------------------------------------------------------------ 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: proper_subsumption, default: false ------------------------------------------------------------------------------ Use 'proper' subsumption - normally the E-hyper tableaux calculus uses the special form called non-proper subsumption. Set this flag to true to use normal subsumption (only effective during back subsumption, forward subsumption uses non-proper subsumption). ------------------------------------------------------------------------------ Flag: learn_closing_lemmas, default: false ------------------------------------------------------------------------------ If set to true (default false), lemmas will be learnt from closed branches. See the commands 'add_closing_lemmas_to_input', 'print_closing_lemmas', 'print_tptp_fof_closing_lemmas' and 'clear_closing_lemmas' for how to utilize these lemmas. ------------------------------------------------------------------------------ Flag: keep_symbol_data, default: false ------------------------------------------------------------------------------ When set to true (default false), the prover will remember the symbols it has read even in one of the 'read_and_print_only' modes. This allows creating equality axioms with the 'add_equality_axioms' command even during 'read_and_print_only'. ------------------------------------------------------------------------------ Flag: check_input_subsumption, default: true ------------------------------------------------------------------------------ Perform subsumption checks among input clauses. This can take a lot of time for very large input sets, so if the input is known to contain no redundant clauses, then switching this off may be useful. ------------------------------------------------------------------------------ Flag: subterm_indexing, default: true ------------------------------------------------------------------------------ Enable or disable indexing of subterms. Disabling this indexing effectively disables rewriting (superposition) based inferences. ------------------------------------------------------------------------------ Flag: wait_for_webservices, default: true ------------------------------------------------------------------------------ If set to true, E-KRHyper will wait indefinitely for any pending webservice answers before declaring a model. If set to false, then E-KRHyper will only check each pending webservice query once when no other inferences are possible, then declare a model. ------------------------------------------------------------------------------ Flag: prevent_reloading, default: false ------------------------------------------------------------------------------ If set to true, a file will not be loaded more than once. Any attempt to load a file after it has already been loaded will have no effect. ------------------------------------------------------------------------------ Flag: tptp_fof_negate_conjectures, default: true ------------------------------------------------------------------------------ Negate first order formulas in the tptp-format, if they are identified as conjectures. Default is true. ------------------------------------------------------------------------------ Flag: tptp_fof_compute_answer_predicate, default: false ------------------------------------------------------------------------------ Compute an answer predicate. Normally, a first order conjecture in the format is negated, taking the form 'false :- .' If a particular variable 'FOCUS' in is of interest, then the clause can be transformed into '$answer(FOCUS) :- .' by setting this flag to true. Starting the derivation with the command '#(run('$answer'/1)).' instead of the regular '#(run).' will then cause the tableau calculation until the first derivation of an '$answer'-unit. The value of the answer variable can then be obtained with the command '#(print_extent('$answer'/1)).' ------------------------------------------------------------------------------ Flag: tptp_fof_compute_abductive_answer_predicate, default: false ------------------------------------------------------------------------------ Experimental - adds clauses which compute abductively relaxed answer predicate units of the type '$abductive_answer/3'. Requires a connection to the proxy-based webservice interface (i.e. the new clauses utilize $$wsq-literals with the '$$proxy' argument). Also, the 'tptp_fof_compute_answer_predicate' flag must be set to true. ------------------------------------------------------------------------------ Flag: tptp_fof_compute_partial_answers, default: false ------------------------------------------------------------------------------ This causes the computation of special units which represent failed closing attempts on a conjecture clause. These units have the predicate '$partial_answer/3'. The first argument is a list of the successfully unified negative literals of the clause. The second argument is a list of variable bindings, the unifier computed so far. The last argument is a list of the negative literals which have not been unified. The first of these is the one where unification failed, causing this closing attempt to stop. '$partial_answer/3' is thus a second order predicate and should be treated with care. When halting a computation due to a timeout, the partial answers may provide hints at the problems in finding a proof. ------------------------------------------------------------------------------ Flag: ensure_safe_filenames, default: false ------------------------------------------------------------------------------ If the filenames of files about to be loaded into E-KRHyper contain unusual characters which may be illegal in some operating systems, then these characters will be replaced by the underline character ('_'). For example, Windows does not allow the colon character within filenames while Linux does, so files transferred from Linux to Windows may experience a filename change. Any 'load' commands within these files may still be referring to the original, now illegal names, so E-KRHyper would not find these files any more. With the flag set to true, the (illegal) filename within the 'load' command will be changed to the legal one and the correct file will be loaded. ------------------------------------------------------------------------------ Flag: print_safe_fof, default: false ------------------------------------------------------------------------------ Experimental! Converts any TPTP-FOF input into a 'safe form', i.e. various peculiarities will be removed and all names will be unique. ------------------------------------------------------------------------------ Flag: anonymous_safe_fof, default: false ------------------------------------------------------------------------------ Experimental! Affects the behaviour initiated by the print_safe_fof flag. If set to true, names will not only be unique, but standardized into an unrecognizable form. ------------------------------------------------------------------------------ Flag: pretend_range_restricted_input, default: false ------------------------------------------------------------------------------ Pretend that the input clause set is range restricted, thus disabling making it range restricted. ------------------------------------------------------------------------------ Flag: dl_blocking, default: false ------------------------------------------------------------------------------ Use DL Blocking when evaluating $$atleast-literals. ------------------------------------------------------------------------------ Flag: back_subsumption_within_news, default: false ------------------------------------------------------------------------------ Use back subsumption within the set of newly derived clauses. ------------------------------------------------------------------------------ Flag: premise_redundancy, default: true ------------------------------------------------------------------------------ Discards new clauses if some of their premises have become redundant in the same evaluation round. Experimental, and automatically disables back_subsumption_within_news. ------------------------------------------------------------------------------ Flag: sort_heads, default: true ------------------------------------------------------------------------------ Sort disjunctive heads heuristically. ------------------------------------------------------------------------------ Flag: check_disjunctions_are_ground, default: false ------------------------------------------------------------------------------ Verify at runtime for each derived disjunction that it is 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: true ------------------------------------------------------------------------------ Generate proof terms for derived facts. ------------------------------------------------------------------------------ Flag: keep_proof_substitutions_flag, default: false ------------------------------------------------------------------------------ Substitutions used during the derivation will be stored inside the proof terms. Specifically, the 'hyper' proof terms will receive a new, additional third argument consisting of a term list that represents the substitution. The other arguments are shifted to the right, i.e. the normal third argument becomes the fourth and so on. Substitutions are only kept for 'hyper' proof terms so far, not for equality based inferences like superposition, nor for simplifications. it is recommended to use this option only on equality-free problems, and to switch off the 'simplify_flag', in order to get proofs consisting only of inferences which get their substitutions listed. ------------------------------------------------------------------------------ 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: echo_command, default: false ------------------------------------------------------------------------------ Print each command statement before it is processed. ------------------------------------------------------------------------------ Flag: debug, default: false ------------------------------------------------------------------------------ Debug mode. Print extra information about clause compilation. ------------------------------------------------------------------------------ Flag: sup_left_flag, default: true ------------------------------------------------------------------------------ Use superposition left. If set to false, ordered paramodulation left will be used. ------------------------------------------------------------------------------ Flag: unit_sup_right_flag, default: true ------------------------------------------------------------------------------ Use unit superposition right. If set to false, ordered paramodulation right will be used. ------------------------------------------------------------------------------ Flag: prefer_dom_literals_flag, default: false ------------------------------------------------------------------------------ Select domain literals first. Used for finite model computation. Experimental! Must be set to true before clauses are entered. Should not be changed later, restart E-KRHyper instead. ------------------------------------------------------------------------------ Flag: delay_dom_enumeration_flag, default: true ------------------------------------------------------------------------------ If set to true, E-KRHyper will attempt to delay the domain enumeration as long as possible. It remains sound and complete. ------------------------------------------------------------------------------ Flag: sort_clauses_for_answer_computation, default: false ------------------------------------------------------------------------------ Experimental! The clauses will be sorted in a way optimized for answer computation. Delta clauses will be used in the first round. Delta clause literals will be sorted according to body_sorting_method 1. ------------------------------------------------------------------------------ Flag: finite_model_transformation_flag, default: false ------------------------------------------------------------------------------ Apply finite model transformation. If set to true, clauses will be range-restricted, the domain will be finite and the Herbrand universe will be enumerated. The flag affects the entire run of E-KRHyper. If the transformation is to be applied, then the flag must be set to true before the first clauses are entered, and the flag should not be set to false again later on. ------------------------------------------------------------------------------ Flag: full_branch_redundancy_flag, default: true ------------------------------------------------------------------------------ Use full branch redundancy handling. If set to true, any facts and clauses within the current branch may be declared redundant, disregarding the E-Hyper calculus rule about not crossing decision nodes. If set to false, the calculus will be performed strictly as defined. Note that there is no efficiency advantage in setting the flag to false, the option is merely included to allow for a strict calculus implementation. The default value is true. ------------------------------------------------------------------------------ Flag: hyperextension_flag, default: true ------------------------------------------------------------------------------ Use hyperextension. If set to true, the hyperextension inference of the (non-equational) Hyper-tableaux calculus will be used for resolving away non-equational literals, even when the program is running in E-Hyper mode (i.e. there are equational literals present). The hyperextension inference is equivalent to a series of sup-left and ref-inferences in the E-Hyper calculus, so this has no effect on soundness and completeness, and it is faster than treating all literals as equations. However, to allow for a strict E-Hyper calculus implementation, usage of the hyperextension can be switched off by setting this flag to false. In this case, all non-equational literals will be converted to equations, and only the inferences detailed in the E-Ehyper calculus description will be used. Note that in this case you should ensure that the input contains no predicates and functions sharingarity and name, because this distinction will be lost during the conversion to equations. ------------------------------------------------------------------------------ Flag: simplify_flag, default: true ------------------------------------------------------------------------------ Use simplification. Simplification will exhaustively simplify clauses using demodulation, subsumption, resolution and other operations which are not necessarily explicit parts of the calculus. Soundness and refutational completeness are preserved and performance is improved. However, this may negatively affect model enumeration (for example by 'merging' models due to simplifying them into the same form), so it may be better to switch this flag off for these purposes. Also, simplification of a clause will usually appear as a single inference in the proof output, even though this inference may actually consist of multiple applications of demodulation etc. ------------------------------------------------------------------------------ Flag: simplify_input_flag, default: true ------------------------------------------------------------------------------ Use input simplification. Input clauses will be simplified as soon as they are entered. ------------------------------------------------------------------------------ Flag: simplify_immediately_flag, default: true ------------------------------------------------------------------------------ If true, inference results will be simplified immediately, before any weight checks ------------------------------------------------------------------------------ Flag: store_overweight_flag, default: true ------------------------------------------------------------------------------ If true, overweight results will be kept (but not used for inferencing). In the case of a fixed point they will be simplified, and if all of them are redundant, then there is no need to increase the weight limit and recompute. This increases the chance to find models, but requires more memory. ------------------------------------------------------------------------------ Flag: szs_output_flag, default: false ------------------------------------------------------------------------------ Display SZS-conforming output. If set to true, each result printout will include one line displaying the result in SZS-syntax. If the input clause set is found to be satisfiable, then the line will read: '% SZS status Satisfiable' Otherwise the line will read: '% SZS status Unsatisfiable' Notes: When enumerating models, a 'Closed' result indicates that no further models exist. The SZS status may still be satisfiable, provided that at least one model has been found. The SZS status line is not commented out like other E-KRHyper output, to conform with CASC-regulations. The output of E-KRHyper will therefore no longer be Prolog-readable if this flag is set to true. ------------------------------------------------------------------------------ Flag: szs_quiet_timeout_flag, default: false ------------------------------------------------------------------------------ Do not display an SZS timeout result if an internal timeout is reached, even if generally set to produce SZS output. ------------------------------------------------------------------------------ Flag: szs_fof_flag, default: false ------------------------------------------------------------------------------ Will be set to true automatically when the input contains first-order formulaic TPTP input. This will change the SZS output to that for a fof-problem. Manual setting is not recommended. ------------------------------------------------------------------------------ Flag: szs_as_comments_flag, default: true ------------------------------------------------------------------------------ Per default SZS results will be printed as Prolog-style comments '% ...'. By setting this flag to false, the ouput will be printed without the comment symbol. ------------------------------------------------------------------------------ Flag: szs_conjecture_flag, default: false ------------------------------------------------------------------------------ Will be set to true automatically when the input contains first-order formulaic TPTP input with a conjecture. This will change the SZS output to that for a fof-problem. Manual setting is not recommended. ------------------------------------------------------------------------------ Flag: partitioning_flag, default: false ------------------------------------------------------------------------------ If set to true, then those rules/clauses which are definitely not required for the computation of an answer clause (TPTP conjecture) will be treated as redundant and not participate in the tableau derivation. ------------------------------------------------------------------------------ Flag: auto_partitioning_flag, default: false ------------------------------------------------------------------------------ If set to true, then E-KRHyper will decide on its own when to partition. Currently this will be done for problems which contain no equality. ------------------------------------------------------------------------------ Flag: block_equation_stratification_flag, default: true ------------------------------------------------------------------------------ Prevents the derivation of equations in strata after the first. If set to true, clauses with equations in the head and body literals requiring stratification (like default negation) are not allowed, and their presence will halt the computation. Default setting is true. ------------------------------------------------------------------------------ Flag: compute_partial_answers, default: false ------------------------------------------------------------------------------ Supposed to be used in conjunction with the 'compute_answer_for_tptp_fof_variable' command, and will have no effect otherwise. When set to true, in addition to the regular answer-units E-KRHyper will compute units for partial answers. An answer unit is derived when all body literals of the clausified conjecture unify with the extent, and a partial answer unit is derived when a subset of the body literals unify with the extent. In the case of of a timeout or any other interruption of the tableau derivation process, the partial answer units may provide information regarding how close the system was to a final answer. A partial answer unit uses the partial answer predicate '$partial_answer/1'. This is a second order predicate, and its single argument is a list of the unified body literals. ------------------------------------------------------------------------------ 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. ------------------------------------------------------------------------------ Flag: limit_block, default: false ------------------------------------------------------------------------------ If set to true, any exceeded limit (timer or memory) will lead to blocking of subsequent input. Any subsequent input will not be processed. Instead the following message will be printed: 'EKRH-Warning: Limit exceeded, clear limit block first.' The command '#(clear_limit_block)' is the only input that will be executed once a block is in place, it clears the block, until the next exceeded limit blocks again. ============================================================================== Parameters ============================================================================== ------------------------------------------------------------------------------ Parameter: max_weight_initial, default: 3 ------------------------------------------------------------------------------ The initial weight limit for inferred literals. If -1, weight handling is not used. Alternatively the initial weight limit can be determined automatically with the command 'automatic_max_weight_initial'. For infinite Herbrand domains, weight handling can be required to ensure refutational completeness and `finite-branch-model' completeness. ------------------------------------------------------------------------------ Parameter: max_proof_depth, default: -1 ------------------------------------------------------------------------------ Halts the computation if a proof would exceed this value. If -1 (default setting), no proof depth restriction is used. ------------------------------------------------------------------------------ Parameter: max_weight_limit, default: -1 ------------------------------------------------------------------------------ Halts the computation if the weight limit exceeds this value. If -1 (default setting), no such restriction is used. ------------------------------------------------------------------------------ Parameter: max_lookahead_size, default: -1 ------------------------------------------------------------------------------ The maximum number of units stored in the special lookahead index that is used for optimization of the Given Clause Algorithm. If -1 (default setting), no size restriction is used. ------------------------------------------------------------------------------ Parameter: dom_literal_weight_factor, default: 5 ------------------------------------------------------------------------------ It can be beneficial to slow down the enumeration of the Herbrand universe by assigning a larger weight to the domain literals. This parameter specifies a multiplier which is applied to the actual weight of domain literals. ------------------------------------------------------------------------------ Parameter: lemmas_at_weight, default: -1 ------------------------------------------------------------------------------ When using the '#(save_lemmas)'-command, only those lemmas are saved which were derived while the term weight limit did not exceed the value of this parameter. Lemmas derived later are ignored. If -1 (default setting), then all lemmas are preserved. ------------------------------------------------------------------------------ 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: finite_model_transformation_domain_size, default: 0 ------------------------------------------------------------------------------ Sets the current domain size parameter for the finite model transformation. Setting the parameter to a positive integer will set the domain size to that number. Setting the parameter to 0 will set the domain size to the number of constants in the current input clause set. This parameter has no effect unless the 'finite_model_transformation_flag' has been set. ------------------------------------------------------------------------------ Parameter: term_ordering, default: 0 ------------------------------------------------------------------------------ Used to select the term ordering. Settings are: 0 - LRPO (lexicographic recursive path ordering) 1 - KBO (Knuth-Bendix ordering ) The default setting is 0 (LRPO). ------------------------------------------------------------------------------ Parameter: read_and_print_only, default: 0 ------------------------------------------------------------------------------ This parameter can be used to utilize E-KRHyper as a converter. The default setting for this parameter is 0, this is the setting when E-KRHyper is supposed to reason on its input problems. If set to 1, input files will be read and their logic input will be printed in prefix Protein-syntax (i.e. canonical Prolog). This input will not be available for reasoning, E-KRHyper discards it immediately after printing. If set to 2, E-KRHyper behaves as when set to 1, except that infix Protein syntax is used for printing. This is not Prolog compatible for non-Horn clauses. ------------------------------------------------------------------------------ Parameter: timeout_termination_method, default: 0 ------------------------------------------------------------------------------ Deprecated. Determines the behaviour of E-KRHyper whenever a timeout induced by a timer (virtual and wallclock) occurs. The following values can be used: 0 - E-KRHyper terminates. 1 - The execution of the current command/statement ends, and E-KRHyper returns to the interactive prompt. If the timeout interrupted a tableau derivation, then any partial results are discarded, and the most recent input state is restored. 2 - Analogous to 1, except that partial results are not discarded. Note that while these partial results can be accessed like a model ('#(print_extent)' etc.), they most likely do not represent a model. ------------------------------------------------------------------------------ Parameter: limit_termination_method, default: 0 ------------------------------------------------------------------------------ Determines the behaviour of E-KRHyper whenever a given limit (virtual or wallclock timer, memory limit) has been reached. The following values can be used: 0 - E-KRHyper terminates. 1 - The execution of the current command/statement ends, and E-KRHyper returns to the interactive prompt. If a tableau derivation has been interrupted, then any partial results are discarded, and the most recent input state is restored. 2 - Analogous to 1, except that partial results are not discarded. Note that while these partial results can be accessed like a model ('#(print_extent)' etc.), they most likely do not represent a model. ------------------------------------------------------------------------------ Parameter: interrupt_termination_method, default: 0 ------------------------------------------------------------------------------ Determines the behaviour of E-KRHyper for a SIGINT signal (Strg + C). The following values can be used: 0 - The execution of the current command/statement ends, and E-KRHyper returns to the interactive prompt. If a tableau derivation has been interrupted, then any partial results are discarded, and the most recent input state is restored. If no command/statement is being executed at the time of the SIGINT signal (i.e., E-KRHyper is in the interactive prompt), E-KRHyper terminates. 1 - E-KRHyper terminates. ------------------------------------------------------------------------------ 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. 3 - experimental heuristics. ------------------------------------------------------------------------------ Parameter: input_type, default: 0 ------------------------------------------------------------------------------ Determines the format of the input. E-KRHyper can read two input formats, tme and tptp. The default setting is to read all input as tme. Exception: files with the extension '.p' or '.ax' will be read as tptp. Setting the input parameter manually allows to override the default behaviour. The following values can be used: 0 - all input is read as tme, except for tptp-files. 1 - all input is read as tme. 2 - all input is read as tptp. 3 - backward compability mode: all input is read as tme, and it must be in canonical Prolog-syntax as ensured by the preprocessor scripts. Reading tptp as tme or vice versa may cause parsing errors. Command statements are always parsed correctly, regardless of input type setting. Note that a change of input type will only take effect after the current file has been read. Having multiple formats within one file is not recommended. ------------------------------------------------------------------------------ Parameter: relaxation_lookahead, default: 0 ------------------------------------------------------------------------------ TODO ------------------------------------------------------------------------------ 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. ------------------------------------------------------------------------------ Parameter: print_input_count, default: 0 ------------------------------------------------------------------------------ If set to n>0, then E-KRHyper will print the count of currently processed input clauses/formulae after every n-th clause/formula. Setting this parameter to 0 (default) disables this printout. ------------------------------------------------------------------------------ Parameter: tptp_qa, default: 0 ------------------------------------------------------------------------------ This is used to enable the special TPTP question answering mode as used in CASC. It should not be confused with the other answer-related flags. The following values can be used: 0 - (default), no answer extraction. 1 - any special conjecture formulas of the 'question' type will be used for answer extraction, i.e. their variable bindings will be returned in TPTP answer format if a proof is found. 2 - similar to 1, but even normal conjecture-type formulas will be used for answer extraction. ------------------------------------------------------------------------------ Parameter: tptp_qa_answer_type, default: 0 ------------------------------------------------------------------------------ This defines which TPTP answer syntax is used when 'tptp_qa' is in use. The following values can be used: 0 - (default), formulae form, 1 - tuple answer form. ------------------------------------------------------------------------------ Parameter: given_clause_algorithm_fifo_pick, default: 5 ------------------------------------------------------------------------------ When using the Given Clause Algorithm and this parameter is set to some positive n, then every n-th selection will simply be done by age rather than by weight and size heuristics. ============================================================================== 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.