Module Ac

module Ac: sig  end

Inference system for theories with single AC symbol
Author(s): Harald Ruess, N. Shankar

module type SIG = sig  end

Specification of a signature th with one binary, associative-commutative (AC) function symbol f.

module type TERM = sig  end

Canonizer and iterators for AC theories.

module Ops: functor (Sig : SIG) -> Can.OPS

Various operations on flat equalities.

module Make: functor (Sig : SIG) -> TERM

Canonizer for a theory with one AC symbol, say *.

module T: functor (Sig : SIG) -> Can.T

Specification of a theory with a single AC symbol by means of canonizers and ground completion functions.

module Infsys: functor (Sig : SIG) -> sig  end

Inference system for a theory with a single AC symbol.