package logtk

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

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