• Coq

  • Referenced in 1828 articles [sw00161]
  • management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems ... machine-checked proofs. Typical applications include the formalization of programming languages semantics (e.g. the CompCert ... EAL7 certification in industrial context), the formalization of mathematics (e.g. the full formalization...
  • Isabelle/HOL

  • Referenced in 978 articles [sw01569]
  • assistant. It allows mathematical formulas to be expressed in a formal language and provides tools ... calculus. The main application is the formalization of mathematical proofs and in particular formal verification...
  • Isabelle

  • Referenced in 622 articles [sw00454]
  • assistant. It allows mathematical formulas to be expressed in a formal language and provides tools ... calculus. The main application is the formalization of mathematical proofs and in particular formal verification...
  • HOL Light

  • Referenced in 296 articles [sw06580]
  • some non-trivial tasks in the formalization of mathematics and industrial formal verification...
  • LEGO

  • Referenced in 107 articles [sw09685]
  • bringing the level of formalization closer to that of informal mathematics. The higher-order power ... types, provide an expressive language for formalization of mathematical problems and program specification and development...
  • Isar

  • Referenced in 144 articles [sw04599]
  • Despite this success in actually formalizing parts of mathematics and computer science, there are still ... semi-automated reasoning (Isar) approach to readable formal proof documents sets out to bridge...
  • Isabelle/ZF

  • Referenced in 62 articles [sw04973]
  • assistant. It allows mathematical formulas to be expressed in a formal language and provides tools ... calculus. The main application is the formalization of mathematical proofs and in particular formal verification...
  • MPTP 0.2

  • Referenced in 45 articles [sw02589]
  • project is to make the large formal Mizar Mathematical Library (MML) available to current first ... Mizar proof constructs into the TPTP formalism. The proofs using second-order Mizar schemes ... inductive or deductive system trained on formal mathematics can be sometimes smarter than MML authors...
  • ETPS

  • Referenced in 157 articles [sw06302]
  • partial automation of various mathematical activities, promoting development of formal theories in a wide variety ... textbook: Peter B. Andrews, An Introduction to Mathematical Logic and Type Theory: To Truth Through ... ETPS: A System to Help Students Write Formal Proofs (postscript...
  • Nuprl

  • Referenced in 390 articles [sw06751]
  • system is a framework for reasoning about mathematics and programming. Over the years its design ... base and supports the cooperation of independent formal tools...
  • Flyspeck

  • Referenced in 114 articles [sw10277]
  • Flyspeck informal mathematical text as a narrative linked to the formal development. To make this...
  • C-CoRN

  • Referenced in 34 articles [sw06752]
  • computer based library of constructive mathematics, formalized in the theorem prover Coq. Background: There ... this: we put mathematics on a computer in an active (formalized ... constructive theorem prover), but mainly because constructive mathematics has the additional bonus of providing (actual ... CoRN grew out of the FTA project, formalizing the Fundamental Theorem of Algebra...
  • Ott

  • Referenced in 31 articles [sw00663]
  • either for informal mathematics or the formal mathematics of a proof assistant -- make it much...
  • MoMM

  • Referenced in 33 articles [sw04655]
  • world’s largest body of formalized mathematics - the Mizar Mathematical Library (MML), which uses...
  • MMT

  • Referenced in 48 articles [sw07136]
  • provides an interface layer between formally rigorous mathematical systems, and knowledge management services which...
  • MPTP

  • Referenced in 24 articles [sw02489]
  • existence of large integral bodies of formalized mathematics. Then we proceed to describe the implementation ... makes the largest existing corpus of formalized mathematics available to theorem provers. MPTP (Mizar Problems...
  • Matita

  • Referenced in 71 articles [sw06140]
  • machine collaboration. It provides a formal language where mathematical definitions, executable algorithms and theorems cohexist...
  • MBase

  • Referenced in 17 articles [sw08724]
  • that offers a universal repository of formalized mathematics where the formal representation allows semantics-based ... propose a methodology for developing representation formalisms for mathematical knowledge bases. We propose to concretely ... that is well-suited both for formalizing mathematical practice and supporting efficient inference services. This...
  • UniMath

  • Referenced in 15 articles [sw15140]
  • UniMath - a library of mathematics formalized in the univalent style. he univalent style of formalization ... level 3 one can efficiently formalize mathematics at the level of categories etc. Univalent style ... allows to directly formalize constructive mathematics and to formalize classical mathematics by adding the excluded ... growing library of constructive mathematics formalized in the univalent style using a small subset...
  • MegaWave

  • Referenced in 27 articles [sw04428]
  • inspired from and are a mathematical formalization of the Gestalt theory. Gestalt theory, which ... never been formalized is a rigorous realm of vision psychology developed between ... From the mathematical viewpoint the closest field to it is stochastic geometry, involving basic probability...