Module Comp


module Comp: sig .. end

Knuth-Bendix completion



type ers = Equation.EqnSet.t * Rule.RulSet.t 
val fprintf : ers Useful.fprintf
exception Unorientable of Equation.EqnSet.t
val step : Rule.RulSet.t -> Term.term Order.cmp -> ers -> ers
Completion step
val complete_n : Rule.RulSet.t -> Term.term Order.cmp -> int -> ers -> ers * int
Kimited completion. n is the maximal number of completion steps. rules are assumed oriented by gt
val complete : Rule.RulSet.t -> Term.term Order.cmp -> ers -> ers * int
Full completion. may not terminate. rules are assumed oriented by gt