Coq Cited in 2,035 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,427 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); …
Isabelle Cited in 756 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 630 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 623 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 592 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 430 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); …
OTTER Cited in 333 Documents (1988–2023) Software Authors: Bill McCune; Amor Montano, Jose Alfredo; Miranda Perea, Favio Ezequiel Related Software: TPTP; VAMPIRE; SPASS; … Main Fields: Mathematical logic and foundations (03-XX); Order, lattices, ordered algebraic structures (06-XX); Group theory and generalizations (20-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 305 Documents (1998–2024) Software Authors: Kaufmann, Matt; Moore, Strother Related Software: Isabelle/HOL; Coq; 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); …
LaTeX Cited in 257 Documents (1988–2024) Software Authors: Lamport, Leslie Related Software: TeX; EXPFIT4; Maple; … Main Fields: General and overarching topics; collections (00-XX); Numerical analysis (65-XX); Computer science (68-XX); …
Agda Cited in 255 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); …
Mace4 Cited in 252 Documents (1995–2024) Software Authors: McCune, William Related Software: Prover9; OTTER; TPTP; … Main Fields: Mathematical logic and foundations (03-XX); Order, lattices, ordered algebraic structures (06-XX); General algebraic systems (08-XX); …
kepler98 Cited in 248 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); …
Prover9 Cited in 232 Documents (2006–2024) Software Authors: McCune, William Related Software: Mace4; OTTER; VAMPIRE; … Main Fields: Mathematical logic and foundations (03-XX); Order, lattices, ordered algebraic structures (06-XX); General algebraic systems (08-XX); …
SPASS Cited in 208 Documents (1996–2023) Software Authors: Weidenbach, C; Brahm, U; Hillenbrand, T Related Software: VAMPIRE; TPTP; E Theorem Prover; … Main Fields: Mathematical logic and foundations (03-XX); Group theory and generalizations (20-XX); Computer science (68-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 155 Documents (1997–2022) Software Authors: Buchberger, Bruno; Jebelean, Tudor; Kutsia, Temur; Windsteiger, Wolfgang; Theorema group at RISC institute at JKU Linz; Austria Related Software: Mathematica; Coq; Mizar; … Main Fields: General and overarching topics; collections (00-XX); Mathematical logic and foundations (03-XX); Commutative algebra (13-XX); …
Flyspeck Cited in 135 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; Agda; … 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); …
Kenzo Cited in 73 Documents (2000–2023) Software Authors: Rubio, Julio; Sergeraert, Francis; Yvon Siret; Xavier Dousson Related Software: EAT; ACL2; Coq; … Main Fields: Category theory; homological algebra (18-XX); Group theory and generalizations (20-XX); Algebraic topology (55-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); …
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 44 Documents (2013–2024) 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 44 Documents (2013–2024) 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); …
F5C Cited in 34 Documents (2010–2023) Software Authors: Eder, C.; Perry, J. Related Software: SINGULAR; Maple; Magma; … Main Fields: Combinatorics (05-XX); Number theory (11-XX); Commutative algebra (13-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); …
DeepMath Cited in 19 Documents (2017–2023) Software Authors: Alemi, Alex A.; Chollet, Francois; Een, Niklas; Irving, Geoffrey; Szegedy, Christian; Urban, Josef Related Software: ENIGMA; E Theorem Prover; Mizar; … Main Fields: Mathematical logic and foundations (03-XX); Algebraic geometry (14-XX); Computer science (68-XX)
NASA PVS Cited in 10 Documents (2008–2023) Software Authors: Langley, NASA Related Software: PVS; Isabelle/HOL; Graph Theory; … Main Fields: Combinatorics (05-XX); General algebraic systems (08-XX); Commutative algebra (13-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); …
Jordan Normal Forms Cited in 8 Documents (2016–2024) Software Authors: Thiemann, René; Yamada, Akihisa Related Software: Isabelle/HOL; Archive Formal Proofs; Isabelle; … Main Fields: Mathematical logic and foundations (03-XX); Commutative algebra (13-XX); Numerical analysis (65-XX); …
Echelon Form Cited in 6 Documents (2016–2022) Software Authors: Divasón, Jose; Aransay, Jesús Related Software: Isabelle/HOL; Archive Formal Proofs; Lifting; … Main Fields: Commutative algebra (13-XX); Linear and multilinear algebra; matrix theory (15-XX); Calculus of variations and optimal control; optimization (49-XX); …
Groebner_Bases Cited in 4 Documents (2017–2019) Software Authors: Immler, Fabian; Maletzky, Alexander Related Software: Polynomials; Isabelle/HOL; Deep_Learning; … Main Fields: Commutative algebra (13-XX); Computer science (68-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); …
Count Complex Roots Cited in 2 Documents (2020) Software Authors: Li, Wenda Related Software: Archive Formal Proofs; HOL; Isabelle/HOL; … Main Fields: Number theory (11-XX); Commutative algebra (13-XX); Algebraic geometry (14-XX); …
Gaussian_Integers Cited in 2 Documents (2021–2022) Software Authors: Eberl, M. Related Software: mathlib; Minkowskis_Theorem; Lean; … Main Fields: Number theory (11-XX); Commutative algebra (13-XX); Computer science (68-XX)
Minkowskis_Theorem Cited in 2 Documents (2021–2022) Software Authors: Eberl, M. Related Software: mathlib; Lean; PARI/GP; … Main Fields: Number theory (11-XX); Commutative algebra (13-XX); Computer science (68-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)