package libzipperposition
Install
Dune Dependency
Authors
Maintainers
Sources
md5=97cdb2f90468e9e27c7bbe3b4fb160bb
sha512=fee73369f673a91dfa9e265fc69be08b32235e10a495f3af6477d404fcd01e3452a0d012b150f3d7f97c00af2f6045019ad039164bf698f70d771231cc4efe5d
doc/libzipperposition.calculi/Libzipperposition_calculi/Superposition/Make/index.html
Module Superposition.MakeSource
Parameters
module Env : Libzipperposition.Env.SSignature
module Env = EnvTerm Indices
index for superposition into the set
index for superposition from the set
index for subsumption
Inference Rules
superposition where given clause is active
superposition where given clause is passive
Extraction of clauses from the queue (HO feature)
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.
Same as extract_from_stream_queue with a different extraction heuristic If possible, all clauses are taken from the first stream
Simplifications rules
Check whether the clause is a (syntactic) tautology, ie whether it contains true or "A" and "not A"
semantic tautology deletion, using a congruence closure algorithm to see if negative literals imply some positive Literal.t
Decide on "quoted" "symbols" (which are all distinct)
basic 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
equality subsumption
check whether the clause is subsumed by any clause in the set
list of clauses in the active set that are subsumed by the clause
contextual Literal.t cutting of the given clause by the active set
condensation
Registration
Register rules in the environment