Module Superposition.MakeSource

Parameters

Signature

module Env = Env
Sourcemodule C : module type of Env.C with type t = Env.C.t
Sourcemodule PS : module type of Env.ProofState with type C.t = Env.C.t
Term Indices
Sourceval idx_sup_into : unit -> PS.TermIndex.t

index for superposition into the set

Sourceval idx_sup_from : unit -> PS.TermIndex.t

index for superposition from the set

Sourceval idx_fv : unit -> PS.SubsumptionIndex.t

index for subsumption

Inference Rules
Sourceval infer_active : Env.binary_inf_rule

superposition where given clause is active

Sourceval infer_passive : Env.binary_inf_rule

superposition where given clause is passive

Sourceval infer_equality_resolution : Env.unary_inf_rule
Sourceval infer_equality_factoring : Env.unary_inf_rule
Simplifications rules
Sourceval is_tautology : C.t -> bool

Check whether the clause is a (syntactic) tautology, ie whether it contains true or "A" and "not A"

Sourceval is_semantic_tautology : C.t -> bool

semantic tautology deletion, using a congruence closure algorithm to see if negative literals imply some positive Literal.t

Sourceval handle_distinct_constants : Env.lit_rewrite_rule

Decide on "quoted" "symbols" (which are all distinct)

Sourceval basic_simplify : Env.simplify_rule

basic simplifications (remove duplicate literals, trivial literals, destructive equality resolution...)

Sourceval subsumes : Logtk.Literal.t array -> Logtk.Literal.t array -> bool

subsumes c1 c2 iff c1 subsumes c2

Sourceval subsumes_with : Logtk.Literals.t Logtk.Scoped.t -> Logtk.Literals.t Logtk.Scoped.t -> (Logtk.Subst.FO.t * Logtk.Proof.tag list) option

returns subsuming subst if the first clause subsumes the second one

Sourceval eq_subsumes : Logtk.Literal.t array -> Logtk.Literal.t array -> bool

equality subsumption

Sourceval subsumed_by_active_set : C.t -> bool

check whether the clause is subsumed by any clause in the set

Sourceval subsumed_in_active_set : Env.backward_redundant_rule

list of clauses in the active set that are subsumed by the clause

Sourceval contextual_literal_cutting : Env.simplify_rule

contextual Literal.t cutting of the given clause by the active set

Sourceval condensation : Env.simplify_rule

condensation

Registration
Sourceval register : unit -> unit

Register rules in the environment