• MPTP 0.2

  • Referenced in 50 articles [sw02589]
  • second version of the Mizar Problems for Theorem Proving (MPTP) system and first experimental results ... large formal Mizar Mathematical Library (MML) available to current first-order automated theorem provers (ATPs ... changes in Mizar, in the Mizar-to-TPTP exporter, and in the problem-creating tools ... already complete. About every fifth nonarithmetical theorem is proved in a fully autonomous mode...
  • MPTP

  • Referenced in 26 articles [sw02489]
  • available to theorem provers. MPTP (Mizar Problems for Theorem Proving) is a system for translating ... Mizar Mathematical Library (MML) into untyped first order format suitable for automated theorem provers ... generating theorem proving problems corresponding to MML. The first version generates about 30000 problems from ... complete proofs of Mizar theorems, and about 630000 problems from the simple (one-step) justifications...
  • MoMM

  • Referenced in 34 articles [sw04655]
  • than 2 percent of the main MML theorems are subsumed by others, and that ... percent of the internal lemmas proved by Mizar authors MoMM can provide a useful advice ... their justification. Finally some problems and possible future work are discussed...
  • BliStrTune

  • Referenced in 6 articles [sw18721]
  • Theorem Proving Strategies. Inventing targeted proof search strategies for specific problem sets is a difficult ... task. State-of-the-art automated theorem provers (ATPs) such as E allow a large ... clause weight functions targeted at problems from large ITP libraries. We show that ... performance in solving problems from the Mizar Mathematical Library...
  • Proofwatch

  • Referenced in 4 articles [sw28654]
  • Prover9 theorem provers, both for interactive formalizations and for human-assisted proving of open conjectures ... large set of problems coming from the Mizar library, showing significant improvement...
  • AXIOM

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

  • Referenced in 654 articles [sw00143]
  • CoCoA is a system for Computations in Commutative...
  • Coq

  • Referenced in 1890 articles [sw00161]
  • Coq is a formal proof management system. It...
  • GAP

  • Referenced in 3189 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • Isabelle

  • Referenced in 713 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • Macaulay2

  • Referenced in 1923 articles [sw00537]
  • Macaulay2 is a software system devoted to supporting...
  • Maple

  • Referenced in 5373 articles [sw00545]
  • The result of over 30 years of cutting...
  • Mathematica

  • Referenced in 6355 articles [sw00554]
  • Almost any workflow involves computing results, and that...
  • MiniSat

  • Referenced in 566 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...
  • SINGULAR

  • Referenced in 1508 articles [sw00866]
  • SINGULAR is a Computer Algebra system (CAS) for...
  • Theorema

  • Referenced in 149 articles [sw00961]
  • The software system Theorema provides a uniform logic...
  • MizarMode

  • Referenced in 18 articles [sw01973]
  • MizarMode -- an integrated proof assistance tool for the...
  • OTTER

  • Referenced in 316 articles [sw02904]
  • Our current automated deduction system Otter is designed...
  • VAMPIRE

  • Referenced in 258 articles [sw02918]
  • Vampire 8.0, [RV02,Vor05] is an automatic theorem...