Index of values

Reset the fact base to its original state.

Abolishes the specified predicate, if it exists.

Associate the given declaration object with the given predicate.

apply term context returns a copy of term with the substitution context applied.

Add a unit clause to the given predicate's extent.

Enable sharing of subsequent input terms.

True iff the first binding pattern is stronger or equal to the second, in each position, where Ground is stronger than Bound and Bound is stronger than Free.

Returns a list of clauses, that contains for each body literal with a predicate that appears in delta_predicates, a copy of the clause, with the body literal replaced by ist delta version.

Undefined if the index contains more than the single initial layer.

clear index removes all elements from index.

Remove the association of builtins and predicate symbols for the given symbol_table.

Remove the association of between evaluable functions and symbols for the given symbol_table.

Remove all unit facts from news.

Effect that all input nonunit clauses are removed.

A total ordering function over the keys.

Returns the multiplier of the given context.

copy_term returns a copy of term.

Return some reader for the predicate, e.g.

If term is a variable, dereference_term term context returns its binding in context along with the context too look up bindings in subterms, otherwise the input is returned.

Disable sharing of subsequent input terms and free resources used for sharing.

eval term context returns the result of evaluating the given term in the given context.

Raises BranchClosed.

Return the size of the given predicate's extent in the current model.

fail represents unification failure.

failed trail tests if the given trail is fail.

Ensures that the predicate exists.

find_symbol name arity returns the symbol corresponding to name and arity in the symbol table.

Derive the first model (or a closed tableau).

from_file function filename calls function with stdin temporary redirected from the specified file.

gensym () returns a newly generated symbol that is not maintained by a symbol table.

Get the declarations associated with the given predicate.

DEBUG

Deprecated

Return the output channel where messages are printed.

Get the symbol associated with the given predicate.

Return the current verbosity value.

Note: predicate is assumed to be not a delta predicate.

idb_predicates clauses returns a list of those predicates in clauses which appear in the head of a clause in clauses.

Print information messages, such as statistics, about result to the message output.

Initialize the association of builtins and predicate symbols for the given symbol_table.

Initialize the association of between evaluable functions and symbols for the given symbol_table.

Create a result object.

Prepare a clause for eval_clause.

insert index term entry inserts a new value, entry, into index, associated with key term.

Insert a disjunction into a news object.

Insert a fact into a news object.

interact () runs the KRH processor within a OCaml interpreter.

is_ground term returns true iff term contains no variables.

is_nonvar term returns true iff term is not a variable.

True iff result is open (i.e.

Like iter, but the implementation may remove entries from the table as they are iterated over.

iter_all f store applies f to all terms in the store.

iter_all f index applies f to all entries in the index.

iter_all_and_throw_away f index is similar to iter_all f index, except, that the implementation is allowed to remove entries as they are iterated over from the index.

iter_generalization_candidates f index term context applies f to all those entries in the index, whose keys are variants or more general than term in context, and maybe to more entries in the index.

iter_instance_candidates f index term context applies f to all those entries in the index, whose keys are variants or proper instances of term in context , and maybe to more entries in the index.

iter_unification_candidates f index term applies f to all those entries in the index, whose keys are unifiable with of term in context, and maybe to more entries in the index.

iter_vars f term effects that f is applied to all variables in term.

list_to_ord_set list returns an ordered set with the elements of list, i.e.

If the input fact is unifiable with a fact that has been previously inserted, that entry is returned.

Raises Not_found if the predicate does not exist.

main () runs the KRH processor within a stand alone environment.

Creates an aux for the given Cfg.cfg.

Create a context.

Result is like the given fact, but with the given term.

The index is created with a single initial layer.

make_index () returns a newly created index.

Create a news object.

A proof term aux can be shared in separate calls to proof_term_r_proof, to ensure sharing of subproofs...

Create a symbol table.

make_trail returns an empty trail that is different from fail.

Input must be a list term.

match_terms term1 context1 term2 trail computes the substitution context1 under which term2 is an instance of term1.

LIMIT: The maximum number of distinct variables in a clause.

msg verbosity message outputs the given string as message to stderr, trailed by a newline and flush, if the current verbosity setting is >= verbosity.

Variant of msg that takes a format string with a single argument.

Variant of msg that takes a format string with two arguments.

Variant of msg that takes a format string with three arguments.

Variant of msg that takes a format string with four arguments.

Variant of msg that takes a format string with five arguments.

Variant of msg that takes a format string with eight arguments.

Derive the next model (or a closed tableau) with respect to the given model.

A context that represents the empty binding.

An unusable news object to initialize typed fields.

onto_file function filename calls function with stdout temporary redirected to the specified file.

ord_disjoint set1 set2 is true iff set1 and set2 have no elements in common.

ord_insert set element returns a set with element inserted into it, preserving the order.

ord_intersect set1 set2 is true iff set1 and set2 have at least one element in common.

ord_intersection set1 set2 returns the ordered intersection of set1 and set2.

ord_subset set1 set2 is true iff every element of the ordered set set1 appears in the ordered set set2.

ord_subtract set1 set2 returns the elements in set1 which are not also in set2 as ordered set.

ord_symdiff set1 set2 returns the symmetric difference of set1 and set2 as ordered set.

ord_union set1 set2 returns the ordered union of set1 and set2.

Same as print, but with the output channel as argument.

Return the S-graph representation of the given P-graph.

Return the transposed P-graph.

Raises Not_found if no disjunction that is not subsumed by a unit in the extent is found.

Input must be a term of the form functor/arity.

Print the given term in ISO-Prolog syntax, as by Prolog's write_canonical predicate to stdout.

Same as print, but instead of printing, it returns a string containg the output.

process_news news processes facts in news.

The lexer function.

Parse the given ISO-Prolog clauses.

push element listref effects that element is added to the beginning of the list in listref.

pushnew element listref effects that element is added to the beginning of the list in listref if it is not equal to a member of the list.

Same as pushnew, but physical equality is used to compare list elements.

register_builtin symbol_table name arity implementation effects that the predicate name/arity becomes available as builtin.

register_evaluable symbol_table name arity implementation effects that the function name/arity becomes available as evaluable function.

Undefined if the index contains more than the single initial layer.

remove_variant index term context deletes a single entry which has a variant of term as key from the index.

renumber_variables table term reassigns variable numbers starting from 0 to the variables in term.

Return a P-graph representation of the given S-graph.

save_trail trail returns a representation of the given trail's state, that can be used to undo bindings.

relevant_clauses clauses goal_predicate selects those clauses from clauses which are relevant for computing goal_predicate.

Set the output channel where messages are printed.

Set the current verbosity to the given value.

share_subterms table term returns a variant of term with subterms replaced as far as possible by subterms stored in table.

sort_clauses clauses sorts the clause set according to a heuristics that should allows earlier detection of refutations (branch closings)

The result list is the input list, sorted by Pervasives.compare and with duplicate elements removed.

split_clauses clauses partitions clauses into several sets.

stratify clauses partitions clauses in strata.

subsumes_chk term1 term2 is true iff term2 is an instance of term1.

Iterate over the symbols in the symbol table.

Returns a string represenation "symbol-name/arity" of the given symbol.

term_compare term1 context1 term2 context2 compares term1 in context1 and term2 in context2 according to the ISO-Prolog standard term ordering and returns

Input must be a constant or compound.

Input must be a constant or compound.

term_ident term1 term2 returns true iff both terms are identical, i.e.

Returns true if the input term has ./2 or []/0 as main functor.

Input must be a proper list, i.e.

Return the nth argument of a compound term.

Return a pair of the first and second argument of a compound term.

Input must be a sequence constructed from a binary functor, such that the first argument is the element and the second argument the rest sequence or the last element (which must have a different main functor).

Input must be a list term of Key=Value pairs.

Input must be a list of float terms.

Input must be a list of integer terms.

Input must be a float term.

Input must be an integer term.

Input must be an atom term.

Return the weight of the given term.

Returns a list of vertices of the given S-graph in topological ordering.

undo_bindings trail saved_trail undoes bindings in trail until the state represented by saved_trail is reached.

unify term1 context1 term2 context2 attempts to unify term1 in context1 with term2 in context2.

Returns a possibly optimized variant of the input term (a unit clause), e.g.

variant term1 term2 is true iff both terms are variants.

term is assumed to be term of shape Variable variable.

Returns the transitive closure of the given S-graph as S-graph.

Is > 0 iff an inferred clause has been discarded since it exceeded the weight limit.