module Infsys: sig end
Definition and operations on inference systems.
Author(s): Harald Ruess
module Config: sig end
A configuration (g; e; p) consists of Input facts g,, an equality set e, and, a variable partitioning p.
val g : G.t Pervasives.ref
Global variables for
- current input facts
g
- current variable partitioning
p.
val p : Partition.t Pervasives.ref
module type EQ = sig end
Abstract interface of an inference system for equality theories.
module type ARITH = sig end
Abstract interface of an inference system for arithmetic theories
as an extension of the
Infsys.EQ signature.
module Empty: EQ
Inference system for the empty theory.
val difference : bool Pervasives.ref
module type LEVEL = sig end
Specification of tracer for inference system.
module Trace: functor (I : EQ) -> functor (L : sig end) -> sig end
Tracing rule applications.
module TraceArith: functor (I : ARITH) -> functor (L : sig end) -> sig end
Tracing rule applications.