• z3

  • Referenced in 496 articles [sw04887]
  • integer arithmetic, fixed-size bit-vectors, extensional arrays, uninterpreted functions, and quantifiers. Z3 is integrated...
  • Yices

  • Referenced in 138 articles [sw04436]
  • arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays, fixed-size bit-vectors, 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 higher-order 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]
  • fixed-size 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...
  • Spatial-Yap

  • 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...
  • ADOL-C

  • Referenced in 233 articles [sw00019]
  • ADOL-C: 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...