package logtk

  1. Overview
  2. Docs

Module Logtk.Congruence

Simple and Lightweight Congruence and order

Congruence Closure provides an efficient, lightweight procedure for deciding equality on ground terms (i.e. ignoring variables). Here we have a simple implementation that is mostly used to check if clauses are tautologies w.r.t. equality

module type S = Congruence_intf.S

Functor

module type TERM = sig ... end
module Make (T : TERM) : S with type term = T.t

Common implementations

module FO : S with type term = Term.t