• Mcmt

  • Referenced in 24 articles [sw11911]
  • model checker modulo theories. We describe mcmt, a fully declarative and deductive symbolic model checker ... state systems whose state variables are arrays. Theories specify the properties of the indexes ... safety and fix-points by solving Satisfiability Modulo Theories (SMT) problems. Besides standard SMT techniques...
  • Psyche

  • Referenced in 5 articles [sw28518]
  • inference rules of the logic in natural deduction: it uses instead a focused sequent calculus ... such as those used in sat-modulo-theories solvers. We therefore illustrate Psyche by using...
  • daTac

  • Referenced in 3 articles [sw26325]
  • daTac - Déduction Automatique dans des Théories Associatives-Commutatives...
  • CoCoA

  • Referenced in 654 articles [sw00143]
  • CoCoA is a system for Computations in Commutative...
  • CoCoALib

  • Referenced in 61 articles [sw00144]
  • CoCoALib: A C++ library for computations in commutative...
  • Coq

  • Referenced in 1880 articles [sw00161]
  • Coq is a formal proof management system. It...
  • GAP

  • Referenced in 3154 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • Isabelle

  • Referenced in 698 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • Macaulay2

  • Referenced in 1904 articles [sw00537]
  • Macaulay2 is a software system devoted to supporting...
  • Maple

  • Referenced in 5363 articles [sw00545]
  • The result of over 30 years of cutting...
  • Mathematica

  • Referenced in 6337 articles [sw00554]
  • Almost any workflow involves computing results, and that...
  • MetiTarski

  • Referenced in 52 articles [sw00573]
  • Many inequalities involving the functions ln, exp, sin...
  • MiniSat

  • Referenced in 565 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • Nitpick

  • Referenced in 63 articles [sw00622]
  • Nitpick is a counterexample generator for Isabelle/HOL that...
  • QEPCAD

  • Referenced in 283 articles [sw00752]
  • QEPCAD B: A program for computing with semi...
  • REDUCE

  • Referenced in 746 articles [sw00789]
  • REDUCE is an interactive system for general algebraic...
  • SageMath

  • Referenced in 1970 articles [sw00825]
  • Sage (SageMath) is free, open-source math software...
  • SINGULAR

  • Referenced in 1504 articles [sw00866]
  • SINGULAR is a Computer Algebra system (CAS) for...
  • Theorema

  • Referenced in 149 articles [sw00961]
  • The software system Theorema provides a uniform logic...
  • TPS

  • Referenced in 73 articles [sw00973]
  • TPS and ETPS are, respectively, the Theorem Proving...