Module Tableau

module Tableau: sig .. end

Evaluation of clause sets.

Operations are performed on hypertableau like structures. The fact base is modified by side effects: at a point in time, there is a single "current result" (i.e. "current model") (with respect to a Predicate.predicate_table and NegativeUnits.store).

type result

Represents an open hypertableau fragment or a closed hypertableau.

val initial_result : Cfg.cfg ->
       Predicate.predicate_table ->
       Term.symbol_table -> NegativeUnits.store -> result

Create a result object. The result object is not open (see is_open). It is used to initialize an environment structure (see module Env). It may be seen as representing input facts, without inference rules applied.

val first_result : Cfg.cfg ->
       Predicate.predicate_table ->
       Term.symbol_table -> NegativeUnits.store -> IcSet.clauses -> result

Derive the first model (or a closed tableau).

val next_result : result -> result

Derive the next model (or a closed tableau) with respect to the given model. If the given result is not open, it is returned directly.

val abandon_result : result -> result

Reset the fact base to its original state. The effect of calling next_result on the input result after calling this function is undefined. The result object returned is not open (see is_open). Notice that first_result and next_result automatically reset the fact base if they return a closed result.

val is_open : result -> bool

True iff result is open (i.e. is a model). If result is not open, and has been returned by first_result or next_result, it is closed (i.e. represents a refutation).

val info_msg : result -> unit

Print information messages, such as statistics, about result to the message output. Reported values may only be accurate if this function is called immediately after the result has been returned by first_result or next_result.

type refutation

val get_refutation : result -> refutation

val refutation_to_term : Term.symbol_table -> refutation -> Term.term

val get_l_proof : result -> Fact.l_proof

Deprecated

val print_compiled_rules : Cfg.cfg ->
       Predicate.predicate_table ->
       Term.symbol_table -> NegativeUnits.store -> IcSet.clauses -> unit