Home
last modified time | relevance | path

Searched defs:skolemize (Results 1 – 10 of 10) sorted by relevance

/dports/textproc/py-nltk/nltk-3.4.1/nltk/sem/
H A Dskolemize.py25 def skolemize(expression, univ_scope=None, used_variables=None): function
/dports/lang/purescript/purescript-0.14.5/src/Language/PureScript/TypeChecker/
H A DSkolems.hs49 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 Dq_solver.cpp134 sat::literal solver::skolemize(quantifier* q) { in skolemize() function in q::solver
/dports/math/cvc4/CVC4-1.7/src/theory/bv/
H A Dbv_subtheory_algebraic.cpp838 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 Dcommon_theorem_producer.cpp1131 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 Dterm.py426 def skolemize(self, authority=None, basepath=None): member in BNode
H A Dgraph.py1278 def skolemize(self, new_graph=None, bnode=None, authority=None, basepath=None): member in Graph
/dports/misc/otter/otter-3.3f/source/
H A Dformula.c722 struct formula *skolemize(struct formula *f) in skolemize() function
/dports/math/vampire/vampire-4.5.1/Api/
H A DProblem.cpp1450 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 DUtils.hs1472 skolemize quants = go quants ([], []) function