
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 fixpoints 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 satmodulotheories solvers. We therefore illustrate Psyche by using...

daTac
 Referenced in 3 articles
[sw26325]
 daTac  Déduction Automatique dans des Théories AssociativesCommutatives...

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 SATsolver. 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, opensource 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...