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 human-oriented proofs – have helped Mizar in developing and maintaining a very large body of formalized mathematics. par Mizar is a non-programmable and non-tactical verifier: the proofs are developed in the traditional “write-compile-correct” 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 long-run more readable, maintainable and reusable. This seems to be a crucial factor for a long-term and large-scale formalization effort.MizarMode has been designed with the aim to facilitate this kind of proof development by a number of “code-generating”, “code-browsing” and “code-searching” 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 proof-assistance 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/mizar-mode 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.68103Urban, Josef 2006 all top 5 Cited by 28 Authors 10 Urban, Josef 4 Bancerek, Grzegorz 3 Pąk, Karol 2 Caminati, Marco Bright 2 Kaliszyk, Cezary 2 Naumowicz, Adam 2 Sutcliffe, Geoff 2 Wiedijk, Freek 1 Blanchette, Jasmin Christian 1 Byliński, Czesław 1 Grabowski, Adam 1 Heskes, Tom M. 1 Kerber, Manfred 1 Korniłowicz, Artur 1 Kühlwein, Daniel 1 Lange, Christoph 1 Matuszewski, Roman 1 Mossakowski, Till 1 Nakasho, Kazuhisa 1 Paulson, Lawrence Charles 1 Rosolini, Giuseppe 1 Rowat, Colin 1 Rudnicki, Piotr 1 Shidama, Yasunari 1 Tsivtsivadze, Evgeni 1 van Laarhoven, Twan 1 Wenzel, Makarius 1 Windsteiger, Wolfgang 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 (68-XX) 4 Mathematical logic and foundations (03-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year