
Mizar
 Referenced in 505 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 144 articles
[sw04599]
 existing declarative theorem proving systems (like Mizar), Isar avoids several shortcomings: it is based...

MPTP 0.2
 Referenced in 50 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 48 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 34 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 26 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 (onestep) justifications done by the Mizar checker. We describe the design and structure...

MizarMode
 Referenced in 18 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 24 articles
[sw08206]
 recent research in the context of Mizar and HOL Light, with a number of enhancements...

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

miz3
 Referenced in 11 articles
[sw18631]
 slight variant of the language of the Mizar system, and can be used...

DeepMath
 Referenced in 10 articles
[sw27551]
 premise selection task on the Mizar corpus while avoiding the handengineered features of existing...

Proofwatch
 Referenced in 4 articles
[sw28654]
 large set of problems coming from the Mizar library, showing significant improvement ... previous best set of strategies invented for Mizar by evolutionary methods...

BliStrTune
 Referenced in 5 articles
[sw18721]
 performance in solving problems from the Mizar Mathematical Library...

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...

OTT2MIZ
 Referenced in 1 article
[sw21546]
 ott2miz  otter to Mizar translator...

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 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...

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