package libzipperposition
Install
Dune Dependency
Authors
Maintainers
Sources
md5=7a8e57388083ed763d12d18324c8a086
sha512=5c5ac312ada6b42907d1e91e349454a8375f7bf8165d3459721a40b707a840a3d6b3dc968a66f1040cb4de7aedf5c1c13f3e90b51337eae5ea6de41651d7bd63
doc/libzipperposition.calculi/Libzipperposition_calculi/Superposition/Make/index.html
Module Superposition.Make
Parameters
module Env : Libzipperposition.Env.SSignature
module Env = Envmodule PS : module type of Env.ProofState with type C.t = Env.C.tmodule Stm : Libzipperposition.Stream.S with module C = Env.Cmodule StmQ : Libzipperposition.StreamQueue.S with module Stm = StmTerm Indices
val idx_sup_into : unit -> PS.TermIndex.tindex for superposition into the set
val idx_sup_from : unit -> PS.TermIndex.tindex for superposition from the set
val idx_fv : unit -> PS.SubsumptionIndex.tindex for subsumption
Inference Rules
val infer_active : Env.binary_inf_rulesuperposition where given clause is active
val infer_passive : Env.binary_inf_rulesuperposition where given clause is passive
val infer_equality_resolution : Env.unary_inf_ruleval infer_equality_factoring : Env.unary_inf_ruleExtraction of clauses from the queue (HO feature)
val extract_from_stream_queue : Env.generate_ruleExtracts 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.
val extract_from_stream_queue_fix_stm : Env.generate_ruleSame as extract_from_stream_queue with a different extraction heuristic If possible, all clauses are taken from the first stream
Simplifications rules
val is_tautology : C.t -> boolCheck whether the clause is a (syntactic) tautology, ie whether it contains true or "A" and "not A"
val is_semantic_tautology : C.t -> boolsemantic tautology deletion, using a congruence closure algorithm to see if negative literals imply some positive Literal.t
val handle_distinct_constants : Env.lit_rewrite_ruleDecide on "quoted" "symbols" (which are all distinct)
val basic_simplify : Env.simplify_rulebasic simplifications (remove duplicate literals, trivial literals, destructive equality resolution...)
subsumes c1 c2 iff c1 subsumes c2
val subsumes_with :
Logtk.Literals.t Logtk.Scoped.t ->
Logtk.Literals.t Logtk.Scoped.t ->
(Logtk.Subst.FO.t * Logtk.Proof.tag list) optionreturns subsuming subst if the first clause subsumes the second one
val subsumed_by_active_set : C.t -> boolcheck whether the clause is subsumed by any clause in the set
val subsumed_in_active_set : Env.backward_redundant_rulelist of clauses in the active set that are subsumed by the clause
val contextual_literal_cutting : Env.simplify_rulecontextual Literal.t cutting of the given clause by the active set
val condensation : Env.simplify_rulecondensation