Module Logtk.Rewriting (.ml)

module Rewriting: LogtkRewriting

Ordered rewriting

Although this module is parametrized by an EQUATION module, it only deals with positive equations. Negative equations will be discarded.
module type ORDERED = sig .. end
module MakeOrdered (E : LogtkIndex.EQUATION  with type rhs = LogtkFOTerm.t) : ORDERED  with module E = E

Regular rewriting

module type SIG_TRS = sig .. end
module MakeTRS (I : (E : LogtkIndex.EQUATION) LogtkIndex.UNIT_IDX  with module E = E) : SIG_TRS 
module TRS: SIG_TRS 

FOLogtkFormula rewriting

module FormRW: sig .. end