sci-mathematics

The sci-mathematics category contains mathematical software.

4ti2 | Software package for algebraic, geometric and combinatorial problems |
---|---|

abc | System for sequential logic synthesis and formal verification |

acl2 | Industrial strength theorem prover, logic and programming language |

alectryon | Toolkit for literate programming in Coq |

alt-ergo | Automatic theorem prover |

arb | C library for arbitrary-precision interval arithmetic |

bertini | Software for Numerical Algebraic Geometry |

boolector | Fast SMT solver for bit-vectors, arrays and uninterpreted functions |

btor2tools | Generic parser and tools for the BTOR2 format |

cadabra | Field-theory motivated approach to computer algebra |

cadical | Simplified Satisfiability Solver |

calc | Arbitrary precision C-like arithmetic system |

cgal | C++ library for geometric algorithms and data structures |

cliquer | C routines for finding cliques in an arbitrary weighted graph |

coq | Proof assistant written in O'Caml |

coq-mathcomp | Mathematical Components for the Coq proof assistant |

coq-serapi | Serialization library and protocol for interaction with the Coq proof assistant |

cryptominisat | Advanced SAT solver with C++ and command-line interfaces |

cubicle | Model checker for verifying properties of array-based systems |

cudd | Colorado University binary Decision Diagram library |

cvc4 | Automatic theorem prover for satisfiability modulo theories (SMT) problems |

dataplot | Program for scientific visualization and statistical analyis |

diagrtb | Calculation of some eigenvectors of a large real, symmetrical, matrix |

dsfmt | Double precision SIMD-oriented Fast Mersenne Twister library |

dunshire | Python library to solve linear games over symmetric cones |

easycrypt | Computer-Aided Cryptographic Proofs |

eclib | Programs for elliptic curves defined over the rational numbers |

ent | Random number sequence test and entropy calculation |

eprover | Automated theorem prover for full first-order logic with equality |

euler | Mathematical programming environment |

fann | Fast Artificial Neural Network Library |

flint | Fast Library for Number Theory |

flocq | Formalization of floating-point arithmetic for the Coq proof assistant |

form | Symbolic Manipulation System |

fricas | FriCAS is a fork of Axiom computer algebra system |

frobby | Software system and project for computations with monomial ideals |

gap | System for computational discrete algebra. Core functionality. |

gappa | Tool for verifying floating-point or fixed-point arithmetic |

gappalib-coq | Allows the certificates Gappa generates to be imported by the Coq |

genius | Genius Mathematics Tool and the GEL Language |

geogebra-bin | Mathematics software for geometry |

geomview | Interactive Geometry Viewer |

gfan | Compute Groebner fans and tropical varieties |

giac | A free C++ Computer Algebra System library and its interfaces |

gimps | The Great Internet Mersenne Prime Search |

ginac | C++ library and tools for symbolic calculations |

glpk | GNU Linear Programming Kit |

gmm | Generic C++ template library for sparse, dense and skyline matrices |

gmp-ecm | Elliptic Curve Method for Integer Factorization |

gp2c | A GP to C translator |

gretl | Regression, econometrics and time-series library |

gsl-shell | Lua interactive shell for sci-libs/gsl |

jags | Just Another Gibbs Sampler for Bayesian MCMC simulation |

kind2 | Multi-engine SMT-based automatic model checker |

kissat | Keep-it-simple and clean bare metal SAT solver written in C |

lcalc | Command-line utility and library for L-function computations |

lean | The Lean Theorem Prover |

libpoly | C library for manipulating polynomials |

lpsolve | Mixed Integer Linear Programming (MILP) solver |

lrcalc | Littlewood-Richardson Calculator |

mathematica | Wolfram Mathematica |

mathlib-tools | Development tools for Lean's mathlib |

mathmod | Plot parametric and implicit surfaces |

mathomatic | Automatic algebraic manipulator |

maxima | Free computer algebra environment based on Macsyma |

metamath | Proof verifier based on a minimalistic formalism |

metamath-databases | Sample databases for Metamath |

minisat | Small yet efficient SAT solver with reference paper |

msieve | A C library implementing a suite of algorithms to factor large integers |

nauty | Computing automorphism groups of graphs and digraphs |

nestedsums | A GiNaC-based library for symbolic expansion of certain transcendental functions |

normaliz | Tool for computations in affine monoids and more |

num-utils | A set of programs for dealing with numbers from the command line |

octave | High-level interactive language for numerical computations |

octave-epstk | Graphical output functions for Matlab and Octave |

opensmt | Compact and open-source SMT-solver written in C++ |

otter | An Automated Deduction System |

palp | A Package for Analyzing Lattice Polytopes (PALP) |

pari | Computer-aided number theory C library and tools |

pari-data | Additional dataset packages for PARI |

petsc | Portable, Extensible Toolkit for Scientific Computation |

picosat | SAT solver with proof and core support |

planarity | The edge addition planarity suite of graph algorithms |

plfit | Fit power-law distributions to empirical data |

polymake | Tool for polyhedral geometry and combinatorics |

primecount | Highly optimized CLI and library to count primes |

primesieve | CLI and library for quickly generating prime numbers |

prng | Pseudo-Random Number Generator library |

prover9 | Automated theorem prover for first-order and equational logic |

proverif | Cryptographic protocol verifier in the formal model |

psmt2-frontend | Library to parse and type-check an extension of the SMT-LIB 2 standard |

pspp | Program for statistical analysis of sampled data |

rkward | IDE for the R-project |

rngstreams | Multiple independent streams of pseudo-random numbers |

rw | Compute rank-width decompositions of graphs |

sha1-polyml | implementation of SHA1 is taken from the GNU coreutils package |

singular | Computer algebra system for polynomial computations |

slepc | Scalable Library for Eigenvalue Problem Computations |

smtinterpol | Interpolating SMT-solver computing Craig interpolants for various theories |

spin | An efficient logic-model checker for the verification of multi-threaded code |

stp | Simple Theorem Prover, an efficient SMT solver for bitvectors |

sympow | Symmetric power elliptic curve L-functions |

topcom | Computing Triangulations Of Point Configurations and Oriented Matroids |

twelf | Implementation of the logical framework LF |

unuran | Universal Non-Uniform Random number generator |

vampire | The Vampire Prover, theorem prover for first-order logic |

verifpal | Cryptographic protocol analysis for real-world protocols |

verit | An open, trustable and efficient SMT-prover |

why3 | Platform for deductive program verification |

why3-for-spark | Platform for deductive program verification |

wxmaxima | Graphical frontend to Maxima, using the wxWidgets toolkit |

yacas | General purpose computer algebra system |

yafu | Yet another factoring utility |

yices2 | SMT Solver supporting SMT-LIB and Yices specification language |

z3 | An efficient theorem prover |