Module Equality (.ml)

module Equality: sig .. end

equality by axiomatization

Symbol.equality is fixed as the equality predicate symbol.

type symbol = Symbol.symbol

type clause = Term.clause

val get_axioms : print_axioms:bool -> Problem.problem -> clause list

computes the equality axioms needed for the clause set.

if print_axioms then the axioms are output.