package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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
Extraction of clauses from the queue (HO feature)
Sourceval extract_from_stream_queue : Env.generate_rule

Extracts at most as many clauses from the stream queue as there are streams in the queue. If called with ~full=true extracts only one clause but may loop forever.

Sourceval extract_from_stream_queue_fix_stm : Env.generate_rule

Same as extract_from_stream_queue with a different extraction heuristic If possible, all clauses are taken from the first stream

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct