• Mizar

  • Referenced in 398 articles [sw04704]
  • Mizar System is the only implementation of the Mizar Language. Originally, the Mizar system ... Linux on PowerPC. The whole Mizar system (including verifier) is coded in Pascal using...
  • Isar

  • Referenced in 125 articles [sw04599]
  • existing declarative theorem proving systems (like Mizar), Isar avoids several shortcomings: it is based...
  • MPTP 0.2

  • Referenced in 42 articles [sw02589]
  • paper describes the second version of the Mizar Problems for Theorem Proving (MPTP) system ... project is to make the large formal Mizar Mathematical Library (MML) available to current first ... sorts and deanonymization of abstract terms. Full Mizar proofs are now exported and also encoded ... lemmas and translating of a number of Mizar proof constructs into the TPTP formalism...
  • MML

  • Referenced in 46 articles [sw06970]
  • Licensing the Mizar Mathematical Library (MML). The Mizar Mathematical Library (MML) is a large corpus ... legal status of these efforts of the Mizar community has never been clarified ... policy that suits the peculiar features of Mizar and its community. In this paper ... scientific problems that we addressed for Mizar...
  • MoMM

  • Referenced in 31 articles [sw04655]
  • largest body of formalized mathematics - the Mizar Mathematical Library (MML), which uses a richer formalism ... speed, memory efficiency, dealing with the richer Mizar logic, etc.) required from MoMM ... interactive advisor for the authors of Mizar articles. These tools and choices taken in their ... percent of the internal lemmas proved by Mizar authors MoMM can provide a useful advice...
  • MPTP

  • Referenced in 21 articles [sw02489]
  • formalized mathematics available to theorem provers. MPTP (Mizar Problems for Theorem Proving) is a system ... translating the Mizar Mathematical Library (MML) into untyped first order format suitable for automated theorem ... about 30000 problems from complete proofs of Mizar theorems, and about 630000 problems from ... simple (one-step) justifications done by the Mizar checker. We describe the design and structure...
  • MizarMode

  • Referenced in 15 articles [sw01973]
  • integrated proof assistance tool for the Mizar way of formalizing mathematics The Emacs authoring environment ... Mizar (MizarMode) is today the authoring tool of choice for many (probably the majority ... Mizar authors. This article describes the MizarMode and focuses on the proof assistance functions ... explanation of the design principles behind the Mizar system, and show how these design principles...
  • MaSh

  • Referenced in 17 articles [sw08206]
  • recent research in the context of Mizar and HOL Light, with a number of enhancements...
  • BliStr

  • Referenced in 13 articles [sw16818]
  • CASC@Turing 2012 competition, particularly in the Mizar division. Similar improvement was obtained...
  • miz3

  • Referenced in 8 articles [sw18631]
  • slight variant of the language of the Mizar system, and can be used...
  • DeepMath

  • Referenced in 6 articles [sw27551]
  • premise selection task on the Mizar corpus while avoiding the hand-engineered features of existing...
  • MMode

  • Referenced in 3 articles [sw24341]
  • MMode A Mizar Mode for the proof assistant Coq. Abstract. We present ... similar to the proof language of the Mizar system. These tactics can be used with...
  • BliStrTune

  • Referenced in 3 articles [sw18721]
  • performance in solving problems from the Mizar Mathematical Library...
  • Proofwatch

  • Referenced in 1 article [sw28654]
  • large set of problems coming from the Mizar library, showing significant improvement ... previous best set of strategies invented for Mizar by evolutionary methods...
  • FINANCE5

  • Referenced in 1 article [sw26636]
  • discrete time with the help of the Mizar system...
  • ALCOR

  • Referenced in 3 articles [sw00026]
  • ALCOR - An Algorithmic Concept Recognition Tool to Support...
  • AXIOM

  • Referenced in 165 articles [sw00063]
  • Axiom is a general purpose Computer Algebra system...
  • CoCoA

  • Referenced in 564 articles [sw00143]
  • CoCoA is a system for Computations in Commutative...
  • CoCoALib

  • Referenced in 43 articles [sw00144]
  • CoCoALib: A C++ library for computations in commutative...