×

Found 48 Software Packages (Results 1–48)

Coq

Cited in 2,017 Documents (1993–2024)
Software Authors: Dehlinger, Christophe; Dufourd, Jean-François
Related Software: Isabelle/HOL; Isabelle; HOL; …
Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Category theory; homological algebra (18-XX); …

Isabelle/HOL

Cited in 1,418 Documents (1995–2024)
Software Authors: Naraschewski, Wolfgang; Nipkow, Tobias
Related Software: Coq; Isabelle; HOL; …
Main Fields: Mathematical logic and foundations (03-XX); Combinatorics (05-XX); Computer science (68-XX); …

z3

Cited in 794 Documents (2001–2024)
Software Authors: Research, Microsoft; Moura, Leonardo de; Bjørner, Nikolaj
Related Software: CVC4; SMT-LIB; Yices; …
Main Fields: Mathematical logic and foundations (03-XX); Computer science (68-XX); Operations research, mathematical programming (90-XX); …

MathOverflow

Cited in 827 Documents (2010–2024)
Software Authors: Stack Exchange Inc
Related Software: OEIS; SageMath; GitHub; …
Main Fields: Mathematical logic and foundations (03-XX); Combinatorics (05-XX); Number theory (11-XX); …

Isabelle

Cited in 745 Documents (1990–2024)
Software Authors: Paulson, Larry; Nipkow, Tobias; Wenzel, Makarius
Related Software: Isabelle/HOL; HOL; Coq; …
Main Fields: Mathematical logic and foundations (03-XX); Combinatorics (05-XX); Number theory (11-XX); …

PVS

Cited in 626 Documents (1993–2023)
Software Authors: Owre, Sam; Shankar, Natarajan; Rushby, John
Related Software: Coq; Isabelle/HOL; HOL; …
Main Fields: Mathematical logic and foundations (03-XX); Numerical analysis (65-XX); Computer science (68-XX); …

HOL

Cited in 618 Documents (1985–2024)
Software Authors: Gordon, Michael J. C.
Related Software: Isabelle/HOL; Isabelle; ML; …
Main Fields: Mathematical logic and foundations (03-XX); Combinatorics (05-XX); Number theory (11-XX); …

Mizar

Cited in 562 Documents (1983–2024)
Software Authors: Bancerek, Grzegorz; Bylinski, Czeslaw; Grabowski, Adam; Kornilowicz, Artur; Milewski, Robert; Naumowicz, Adam; Trybulec, Andrzej; Urban, Josef
Related Software: Coq; Isabelle/HOL; HOL Light; …
Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Number theory (11-XX); …

TPTP

Cited in 429 Documents (1994–2024)
Software Authors: Sutcliffe, Geoff; Suttner, Christian
Related Software: VAMPIRE; E Theorem Prover; Isabelle/HOL; …
Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Geometry (51-XX); …

Nuprl

Cited in 425 Documents (1986–2023)
Software Authors: Constable, R. L.; Allen, S. F.; Bromley, H. M.; Cleaveland, W. R.; Cremer, J. F.; Harper, R. W.; Howe, D. J.; Knoblock, T. B.; Mendler, N. P.; Panangaden, P.; Sasaki, J. T.; Smith, S. F.
Related Software: Coq; HOL; Automath; …
Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Category theory; homological algebra (18-XX); …

HOL Light

Cited in 330 Documents (1998–2024)
Software Authors: Harrison, John
Related Software: Coq; Isabelle/HOL; HOL; …
Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Number theory (11-XX); …

ACL2

Cited in 292 Documents (1998–2024)
Software Authors: Kaufmann, Matt; Moore, Strother
Related Software: Coq; Isabelle/HOL; PVS; …
Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Algebraic topology (55-XX); …

Archive Formal Proofs

Cited in 293 Documents (1963–2024)
Software Authors: Blanchette, Jasmin Christian; Haslbeck, Maximilian; Matichuk, Daniel; Nipkow, Tobias
Related Software: Isabelle/HOL; Isabelle; Coq; …
Main Fields: Mathematical logic and foundations (03-XX); Combinatorics (05-XX); Number theory (11-XX); …

OCaml

Cited in 276 Documents (1998–2024)
Software Authors: INRIA; X. Leroy, D. Rémy, J. Vouillon, D. Doligez
Related Software: Coq; Haskell; Isabelle/HOL; …
Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Numerical analysis (65-XX); …

Agda

Cited in 249 Documents (1999–2024)
Software Authors: Norell, Ulf
Related Software: Coq; Isabelle/HOL; Haskell; …
Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Category theory; homological algebra (18-XX); …

kepler98

Cited in 237 Documents (2000–2024)
Software Authors: Hales, Thomas C.; Ferguson, Samuel P.
Related Software: Isabelle/HOL; Flyspeck; Coq; …
Main Fields: Mathematical logic and foundations (03-XX); Number theory (11-XX); Convex and discrete geometry (52-XX); …

E Theorem Prover

Cited in 233 Documents (2001–2023)
Software Authors: Schulz, Stephan
Related Software: VAMPIRE; TPTP; SPASS; …
Main Fields: Mathematical logic and foundations (03-XX); Combinatorics (05-XX); Group theory and generalizations (20-XX); …

NQTHM

Cited in 150 Documents (1979–2022)
Software Authors: Boyer, Robert S.; Moore, J. Strother
Related Software: HOL; ACL2; Coq; …
Main Fields: History and biography (01-XX); Mathematical logic and foundations (03-XX); Group theory and generalizations (20-XX); …

Isar

Cited in 158 Documents (2000–2024)
Software Authors: Wenzel, Makarius
Related Software: Isabelle/HOL; Isabelle; Coq; …
Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Combinatorics (05-XX); …

Theorema

Cited in 151 Documents (1997–2022)
Software Authors: Buchberger, Bruno; Jebelean, Tudor; Kutsia, Temur; Windsteiger, Wolfgang; Theorema group at RISC institute at JKU Linz; Austria
Related Software: Coq; Mathematica; Mizar; …
Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Commutative algebra (13-XX); …

Flyspeck

Cited in 134 Documents (2004–2024)
Software Authors: Hales, Thomas C.; Tankink, Carst; Kaliszyk, Cezary; Urban, Josef; Geuvers, Herman
Related Software: Isabelle/HOL; HOL Light; Coq; …
Main Fields: Mathematical logic and foundations (03-XX); Combinatorics (05-XX); Convex and discrete geometry (52-XX); …

Lean

Cited in 107 Documents (2015–2024)
Software Authors: Microsoft; de Moura, Leonardo; Kong, Soonho; Avigad, Jeremy; van Doorn, Floris; von Raumer, Jakob
Related Software: Coq; Isabelle/HOL; mathlib; …
Main Fields: Mathematical logic and foundations (03-XX); Number theory (11-XX); Category theory; homological algebra (18-XX); …

Isabelle/Isar

Cited in 106 Documents (2002–2024)
Software Authors: Wenzel, Markus; et al.
Related Software: Isabelle/HOL; Isabelle; Isar; …
Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Combinatorics (05-XX); …

OMDoc

Cited in 94 Documents (2001–2023)
Software Authors: Kohlhase, Michael
Related Software: MMT; Coq; Mizar; …
Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Linear and multilinear algebra; matrix theory (15-XX); …

Coq/SSReflect

Cited in 74 Documents (2008–2021)
Software Authors: Center, Microsoft Research-Inria Joint
Related Software: Coq; Isabelle/HOL; Mizar; …
Main Fields: Mathematical logic and foundations (03-XX); Combinatorics (05-XX); Group theory and generalizations (20-XX); …

WolframAlpha

Cited in 64 Documents (2000–2024)
Software Authors: Wolfram Alpha LLC
Related Software: Mathematica; OEIS; Maple; …
Main Fields: General and overarching topics; collections (00-XX); Combinatorics (05-XX); Number theory (11-XX); …

Jordan

Cited in 66 Documents (2007–2022)
Software Authors: Hales, Thomas C.
Related Software: kepler98; HOL Light; Maple; …
Main Fields: Mathematical logic and foundations (03-XX); Field theory and polynomials (12-XX); Commutative algebra (13-XX); …

MetiTarski

Cited in 58 Documents (2008–2024)
Software Authors: Akbarpour, Behzad; Paulson, Lawrence C.
Related Software: QEPCAD; z3; PVS; …
Main Fields: Mathematical logic and foundations (03-XX); Algebraic geometry (14-XX); Numerical analysis (65-XX); …

Locales

Cited in 54 Documents (1999–2024)
Software Authors: Ballarin, Clemens
Related Software: Isabelle/HOL; Isabelle; Archive Formal Proofs; …
Main Fields: Mathematical logic and foundations (03-XX); Combinatorics (05-XX); Algebraic geometry (14-XX); …

Lifting

Cited in 42 Documents (2013–2023)
Software Authors: Huffman, Brian; Kunčar, Ondřej
Related Software: Transfer; Isabelle/HOL; Archive Formal Proofs; …
Main Fields: Mathematical logic and foundations (03-XX); Linear and multilinear algebra; matrix theory (15-XX); Ordinary differential equations (34-XX); …

Transfer

Cited in 42 Documents (2013–2023)
Software Authors: Huffman, Brian; Kunčar, Ondřej
Related Software: Lifting; Isabelle/HOL; Archive Formal Proofs; …
Main Fields: Mathematical logic and foundations (03-XX); Linear and multilinear algebra; matrix theory (15-XX); Ordinary differential equations (34-XX); …

mathlib

Cited in 32 Documents (2020–2024)
Software Authors: van Doorn, Floris; Ebner, Gabriel; Lewis, Robert Y.; The mathlib Community
Related Software: Lean; Coq; Isabelle/HOL; …
Main Fields: Mathematical logic and foundations (03-XX); Order, lattices, ordered algebraic structures (06-XX); Number theory (11-XX); …

CoqHammer

Cited in 28 Documents (2017–2023)
Software Authors: Czajka, Łukasz; Kaliszyk, Cezary
Related Software: Coq; Isabelle/HOL; E Theorem Prover; …
Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Algebraic geometry (14-XX); …

Metamath

Cited in 26 Documents (2003–2023)
Software Authors: Megill, Norman D.
Related Software: Mizar; Isabelle/HOL; Coq; …
Main Fields: Mathematical logic and foundations (03-XX); Number theory (11-XX); Commutative algebra (13-XX); …

Coquelicot

Cited in 25 Documents (2015–2024)
Software Authors: Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume
Related Software: Coq; Isabelle/HOL; Lean; …
Main Fields: Mathematical logic and foundations (03-XX); Real functions (26-XX); Ordinary differential equations (34-XX); …

BIGEBRA

Cited in 22 Documents (1994–2023)
Software Authors: Abłamowicz, Rafał; Fauser, Bertfried
Related Software: CLIFFORD; Maple; CLICAL; …
Main Fields: Number theory (11-XX); Linear and multilinear algebra; matrix theory (15-XX); Associative rings and algebras (16-XX); …

DeepMath

Cited in 17 Documents (2017–2023)
Software Authors: Alemi, Alex A.; Chollet, Francois; Een, Niklas; Irving, Geoffrey; Szegedy, Christian; Urban, Josef
Related Software: E Theorem Prover; Mizar; ENIGMA; …
Main Fields: Mathematical logic and foundations (03-XX); Algebraic geometry (14-XX); Computer science (68-XX)

Berlekamp Zassenhaus

Cited in 10 Documents (2017–2022)
Software Authors: Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa
Related Software: Isabelle/HOL; Isabelle; Coq; …
Main Fields: Number theory (11-XX); Field theory and polynomials (12-XX); Commutative algebra (13-XX); …

SPECTRA

Cited in 9 Documents (2016–2023)
Software Authors: Henrion, Didier; Naldi, Simone; Din, Mohab Safey El
Related Software: FGb; Maple; Kronecker; …
Main Fields: Commutative algebra (13-XX); Algebraic geometry (14-XX); Dynamical systems and ergodic theory (37-XX); …

CAMPARY

Cited in 9 Documents (2016–2023)
Software Authors: Joldes, Mioara; Muller, Jean-Michel; Popescu, Valentina; Tucker, Warwick
Related Software: MPFR; Flocq; LBNL; …
Main Fields: General and overarching topics; collections (00-XX); Algebraic geometry (14-XX); Numerical analysis (65-XX); …

Echelon Form

Cited in 5 Documents (2016–2022)
Software Authors: Divasón, Jose; Aransay, Jesús
Related Software: Isabelle/HOL; Isabelle; Transfer; …
Main Fields: Commutative algebra (13-XX); Linear and multilinear algebra; matrix theory (15-XX); Calculus of variations and optimal control; optimization (49-XX); …

Cayley-Hamilton

Cited in 3 Documents (2016–2022)
Software Authors: Adelsberger, Stephan; Hetzl, Stefan; Pollak, Florian
Related Software: Isabelle; Transfer; Lifting; …
Main Fields: Mathematical logic and foundations (03-XX); Commutative algebra (13-XX); Linear and multilinear algebra; matrix theory (15-XX); …

univsos

Cited in 2 Documents (2018–2019)
Software Authors: Magron, Victor
Related Software: RealCertify; multivsos; PARI/GP; …
Main Fields: Commutative algebra (13-XX); Algebraic geometry (14-XX); Computer science (68-XX)

Vector Spaces

Cited in 2 Documents (2018–2020)
Software Authors: Lee, Holden
Related Software: Berlekamp Zassenhaus; Isabelle/HOL; Sqrt_Babylonian; …
Main Fields: Mathematical logic and foundations (03-XX); Number theory (11-XX); Field theory and polynomials (12-XX); …

Hermite

Cited in 1 Document (2022)
Software Authors: Divasón, Jose; Aransay, Jesús
Related Software: Isabelle; Kenzo; Transfer; …
Main Fields: Commutative algebra (13-XX); Linear and multilinear algebra; matrix theory (15-XX); Computer science (68-XX)

Modular_arithmetic_LLL_and_HNF_algorithms

Cited in 1 Document (2022)
Software Authors: Bottesch, Ralph; Divasón, Jose; Thiemann, René
Related Software: Isabelle; Kenzo; Transfer; …
Main Fields: Commutative algebra (13-XX); Linear and multilinear algebra; matrix theory (15-XX); Computer science (68-XX)

Smith_Normal_Form

Cited in 1 Document (2022)
Software Authors: Divasón, Jose
Related Software: Isabelle; Kenzo; Transfer; …
Main Fields: Commutative algebra (13-XX); Linear and multilinear algebra; matrix theory (15-XX); Computer science (68-XX)

Smooth_Manifolds

Cited in 1 Document (2022)
Software Authors: Immler, Fabian; Zhan, Bohua
Related Software: Isabelle; Kenzo; Transfer; …
Main Fields: Commutative algebra (13-XX); Linear and multilinear algebra; matrix theory (15-XX); Computer science (68-XX)

Filter Results by …

all top 5

Related Software

all top 3

Main Field