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.
Keywords for this software
References in zbMATH (referenced in 12 articles , 1 standard article )
Showing results 1 to 12 of 12.
- Caminati, Marco Bright; Rosolini, Giuseppe: Custom automations in Mizar (2013)
- Lange, Christoph; Caminati, Marco B.; Kerber, Manfred; Mossakowski, Till; Rowat, Colin; Wenzel, Makarius; Windsteiger, Wolfgang: A qualitative comparison of the suitability of four theorem provers for basic auction theory (2013)
- Urban, Josef; Rudnicki, Piotr; Sutcliffe, Geoff: ATP and presentation service for Mizar formalizations (2013)
- Kühlwein, Daniel; van Laarhoven, Twan; Tsivtsivadze, Evgeni; Urban, Josef; Heskes, Tom: Overview and evaluation of premise selection techniques for large theory mathematics (2012)
- Wiedijk, Freek: A synthesis of the procedural and declarative styles of interactive theorem proving (2012)
- Wiedijk, Freek: Pollack-inconsistency (2012)
- Urban, Josef; Sutcliffe, Geoff: Automated reasoning and presentation support for formalizing mathematics in MizAR (2010)
- Urban, Josef; Bancerek, Grzegorz: Presenting and explaining mizar. (2007)
- Bancerek, Grzegorz: Information retrieval and rendering with MML Query (2006)
- Urban, Josef: MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics (2006)
- Urban, Josef: MPTP 0.2: Design, implementation, and initial experiments (2006)
- Urban, Josef: XML-izing Mizar: Making semantic processing and presentation of MML easy (2006)