package logtk

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

Module Logtk.CongruenceSource

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

Sourcemodule type S = Congruence_intf.S

Functor

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

Common implementations

Sourcemodule FO : S with type term = Term.t