Searched defs:skolemize (Results 1 – 10 of 10) sorted by relevance
/dports/textproc/py-nltk/nltk-3.4.1/nltk/sem/ |
H A D | skolemize.py | 25 def skolemize(expression, univ_scope=None, used_variables=None): function
|
/dports/lang/purescript/purescript-0.14.5/src/Language/PureScript/TypeChecker/ |
H A D | Skolems.hs | 49 skolemize ann ident mbK sko scope = replaceTypeVars ident (Skolem ann ident mbK sko scope) function
|
/dports/math/z3/z3-z3-4.8.13/src/sat/smt/ |
H A D | q_solver.cpp | 134 sat::literal solver::skolemize(quantifier* q) { in skolemize() function in q::solver
|
/dports/math/cvc4/CVC4-1.7/src/theory/bv/ |
H A D | bv_subtheory_algebraic.cpp | 838 void ExtractSkolemizer::skolemize(std::vector<WorklistElement>& facts) { in skolemize() function in CVC4::theory::bv::ExtractSkolemizer 925 Node ExtractSkolemizer::skolemize(TNode node) { in skolemize() function in CVC4::theory::bv::ExtractSkolemizer
|
/dports/math/cvc3/cvc3-2.4.1/src/theorem/ |
H A D | common_theorem_producer.cpp | 1131 Expr CommonTheoremProducer::skolemize(const Expr& e) in skolemize() function in CommonTheoremProducer 1223 Theorem CommonTheoremProducer::skolemize(const Theorem& thm) { in skolemize() function in CommonTheoremProducer
|
/dports/textproc/py-rdflib/rdflib-5.0.0/rdflib/ |
H A D | term.py | 426 def skolemize(self, authority=None, basepath=None): member in BNode
|
H A D | graph.py | 1278 def skolemize(self, new_graph=None, bnode=None, authority=None, basepath=None): member in Graph
|
/dports/misc/otter/otter-3.3f/source/ |
H A D | formula.c | 722 struct formula *skolemize(struct formula *f) in skolemize() function
|
/dports/math/vampire/vampire-4.5.1/Api/ |
H A D | Problem.cpp | 1450 Problem Problem::skolemize(int namingThreshold, bool preserveEpr, InliningMode predicateDefinitionI… in skolemize() function in Api::Problem
|
/dports/security/hs-cryptol/cryptol-2.11.0/_cabal_deps/sbv-8.12/Data/SBV/Control/ |
H A D | Utils.hs | 1472 skolemize quants = go quants ([], []) function
|