package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Library
Module
Module type
Parameter
Class
Class type

LogtkFOTerm rewriting

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 : functor (E : LogtkIndex.EQUATION) -> LogtkIndex.UNIT_IDX with module E = E) : SIG_TRS
module TRS : SIG_TRS

FOLogtkFormula rewriting

module FormRW : sig ... end