package libzipperposition
Install
Dune Dependency
Authors
Maintainers
Sources
md5=cc320f66f10555c54822da624419e003
sha512=f8d5f7a5ae790bf0388d74261673803cf375f91f92f7b413b70db1ce5841ef55343a208f98727c8551d66f1840ab892f1c0c943a34861d14d79ce469b235a2f2
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
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