
z3
 Referenced in 496 articles
[sw04887]
 integer arithmetic, fixedsize bitvectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated...

Yices
 Referenced in 138 articles
[sw04436]
 arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays, fixedsize bitvectors, quantifiers...

Satallax
 Referenced in 49 articles
[sw06849]
 Church’s simple type theory with extensionality and choice operators. The SAT solver MiniSat...

LUBM
 Referenced in 20 articles
[sw14975]
 data scalable to an arbitrary size, 14 extensional queries representing a variety of properties...

Orbital library
 Referenced in 13 articles
[sw05562]
 behind the Orbital library is to provide extensional services and components that surround the heart...

KRIPKE
 Referenced in 8 articles
[sw01162]
 dropping the axioms governing the extensional connectives ^ and v from the axiomatizations of these logics...

HOT
 Referenced in 5 articles
[sw13308]
 order theorem prover based on ℋ𝒯ℰ an extensional higherorder tableaux calculus. The first part...

FinFuns
 Referenced in 5 articles
[sw28536]
 logic, they behave like ordinary functions with extensionality. Via the update/constant pattern, a recursion combinator...

ALE
 Referenced in 5 articles
[sw28843]
 types may be declared as having extensional structural identity conditions. Grammars may also interleave unification...

SMTCoq
 Referenced in 3 articles
[sw32310]
 fixedsize bit vectors, functional arrays with extensionality, linear integer arithmetic, and uninterpreted function symbols...

SEMANOL
 Referenced in 3 articles
[sw34033]
 semantics which embraces algorithmic (operational) and extensional (input/output) semantics. Specifications for large contemporary languages have...

SpatialYap
 Referenced in 2 articles
[sw13884]
 these interfaces is restricted to access extensional data in databases in Datalog form, disallowing access...

SONOLAR
 Referenced in 2 articles
[sw26291]
 solver decide the satisfiability. For handling the extensional theory of arrays, the lemmas on demand...

WrapIt
 Referenced in 1 article
[sw01731]
 WrapIt: Automated integration of web databases with extensional overlaps. The world wide web does ... given by the existence of an extensional overlap of the databases...

MXYZPTLK
 Referenced in 5 articles
[sw00008]
 C++ Hacker’s implementation of automatic differentiation...

ADOLC
 Referenced in 233 articles
[sw00019]
 ADOLC: Automatic Differentiation of C/C++. We present...

ANSYS
 Referenced in 655 articles
[sw00044]
 ANSYS offers a comprehensive software suite that spans...

Coq
 Referenced in 1784 articles
[sw00161]
 Coq is a formal proof management system. It...

GRESS
 Referenced in 12 articles
[sw00385]
 GRESS, a preprocessor for sensitivity analysis of Fortran...

PADRE2
 Referenced in 13 articles
[sw00667]
 PADRE2, a Fortran precompiler yielding error estimates and...