MizarMode
swMATH ID:  1973 
Software Authors:  Urban, Josef 
Description:  MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics. The Emacs authoring environment for Mizar (MizarMode) is today the authoring tool of choice for many (probably the majority of) Mizar authors. This article describes the MizarMode and focuses on the proof assistance functions and tools available in it. par We start with the explanation of the design principles behind the Mizar system, and show how these design principles – mainly the concentration on simple and intuitive humanoriented proofs – have helped Mizar in developing and maintaining a very large body of formalized mathematics. par Mizar is a nonprogrammable and nontactical verifier: the proofs are developed in the traditional “writecompilecorrect” software programming loop. While this method is in the beginning more laborious than the methods employed in tactical and programmable proof assistants, it makes the “proof code” in the longrun more readable, maintainable and reusable. This seems to be a crucial factor for a longterm and largescale formalization effort. MizarMode has been designed with the aim to facilitate this kind of proof development by a number of “codegenerating”, “codebrowsing” and “codesearching” methods, and tools programmed or integrated within it. These methods and tools now include, e.g., the automated generation of proof skeletons, semantic browsing of the articles and abstracts, structured viewing, proof advice using trained machine learning tools like the Mizar Proof Advisor, deductive tools like MoMM, etc. We give an overview of these proofassistance tools and their integration in the MizarMode, and also discuss some emerging and future extensions such as integration of external theorem proving assistance. 
Homepage:  http://pdb.finkproject.org/pdb/package.php/mizarmode 
Keywords:  Mizar; MizarMode; proof assistance 
Related Software:  Mizar; MML; MoMM; MPTP 0.2; E Theorem Prover; MPTP; Coq; TPTP; MaLARea; Metamath; Isabelle/HOL; Isar; seL4; ACL2; SPASS; OTTER; Isabelle; MaLeCoP; miz3; Isabelle/Isar 
Cited in:  18 Publications 
Standard Articles
1 Publication describing the Software, including 1 Publication in zbMATH  Year 

MizarMode – an integrated proof assistance tool for the Mizar way of formalizing mathematics. Zbl 1107.68103 Urban, Josef 
2006

all
top 5
Cited by 28 Authors
Cited in 4 Serials
4  Journal of Automated Reasoning 
1  Journal of Applied Logic 
1  Logical Methods in Computer Science 
1  Journal of Formalized Reasoning 
Cited in 3 Fields
18  Computer science (68XX) 
4  Mathematical logic and foundations (03XX) 
1  Game theory, economics, finance, and other social and behavioral sciences (91XX) 