sig
type result
val initial_result :
Cfg.cfg ->
Predicate.predicate_table ->
Term.symbol_table -> NegativeUnits.store -> Tableau.result
val first_result :
Cfg.cfg ->
Predicate.predicate_table ->
Term.symbol_table ->
NegativeUnits.store -> IcSet.clauses -> Tableau.result
val next_result : Tableau.result -> Tableau.result
val abandon_result : Tableau.result -> Tableau.result
val is_open : Tableau.result -> bool
val info_msg : Tableau.result -> unit
type refutation
val get_refutation : Tableau.result -> Tableau.refutation
val refutation_to_term :
Term.symbol_table -> Tableau.refutation -> Term.term
val get_l_proof : Tableau.result -> Fact.l_proof
val print_compiled_rules :
Cfg.cfg ->
Predicate.predicate_table ->
Term.symbol_table -> NegativeUnits.store -> IcSet.clauses -> unit
end