Previous  Up  Next

Module Superposition

module Superposition: sig .. end

Inference and simplification rules for the superposition calculus



Inference rules


val section : Logtk.Util.Section.t
module type S = Superposition_intf.S
val key : (module Superposition.S) Logtk.Flex_state.key
key to access the Env.flex_state. After registration (after calling register), the Env's state contains a mapping from "superposition" to the packed module.
val register : sup:(module Superposition.S) -> unit
Register the superposition module to its Environment's mixtbl. Done automatically by the Superposition.extension.
module Make: 
functor (Env : Env.S) -> S  with module Env = Env

As Extension

Extension named "superposition"
val extension : Extensions.t