package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
type form = LogtkFormula.FO.t
type rule = LogtkFOTerm.t * form

rewrite rule, from left to right

val empty : unit -> t
val add : t -> rule -> t
val add_seq : t -> rule Sequence.t -> t
val add_list : t -> rule list -> t
val add_term_rule : t -> (LogtkFOTerm.t * LogtkFOTerm.t) -> t
val add_term_rules : t -> (LogtkFOTerm.t * LogtkFOTerm.t) list -> t
val to_seq : t -> rule Sequence.t
val of_seq : rule Sequence.t -> t
val of_list : rule list -> t
val size : t -> int
val iter : t -> (rule -> unit) -> unit
val rule_to_form : rule -> form

Convert the rule back to a term

val rewrite_collect : t -> form -> form * rule list

Compute normal form of the formula, and return it together with the list of rules that were used to rewrite.

val rewrite : t -> form -> form

see rewrite_collect