Module Can

module Can: sig  end

Inference system for canonizable, ground confluent theories.
Author(s): Harald Ruess

module type T = sig  end

A canonizable and ground confluent theory th is specified by means of a replacement map f a for replacing uninterpreted subterms of a with f a and canonizing the result,, a theory-specific canonizer;, chainings functions of_var_equal, of_var_diseq, of_var_diseq for keeping equality sets ground confluent by triggering inference rules on pure equalities, variable equalities, and variable disequalities, respectively; and, a branching function disjunction.

module Make: functor (Can : T) -> sig  end

Constructing an inference system from the specification Can of a canonizable and ground confluent theory.

module type OPS = sig  end

Operations for canonizable theories.

module Ops: functor (Can : T) -> OPS

Operations on canonizable theories.