logtk

Core types and algorithms for logic
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library logtk
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