Mizar in a Nutshell

Adam Grabowski, Artur Korniłowicz, Adam Naumowicz · Journal of Formalized Reasoning · 2010

Explore this paper's citation graph

Summary

This paper is intended to be a practical reference manual for basic Mizar terminology which may be helpful to get started using the system.

Type: article
Published: 2010-01-01
Cited by: 186
References: 20
Access: Open access
DOI: https://doi.org/10.6092/issn.1972-5787/1980
OpenAlex: https://openalex.org/W1789208025
Semantic Scholar: https://api.semanticscholar.org/CorpusID:34035680

Keywords

Computer science, Terminology, Programming language, Software engineering, Software

References

Symbolic logic : an introductionRichmond H. Thomason — 1969
ENHANCED PROCESSING OF ADJECTIVES IN MIZARAdam Naumowicz — 2009
Tarski Grothendieck Set TheoryAndrzej Trybulec — 1990
From insight to proof : Festschrift in honour of Andrzej TrybulecAnna Zalewska, Roman Matuszewski — 2007
On a Practical Way of Describing Formal DeductionsKatuzi Ono — 1962
A Comparison of Mizar and IsarMarkus Wenzel, Freek Wiedijk — 2003
Formal Proof SketchesFreek Wiedijk, Fokkink, W. — 2003
Some Features of the Mizar LanguageAndrzej Trybulec — 1993
IZAR : the first 30 yearsR. Matuszewski, P. Rudnicki — 2005
Mizar Light for HOL LightFreek Wiedijk — 2001
Three Tactic Theorem ProvingDon Syme — 1999
Improving Mizar Texts with Properties and RequirementsAdam Naumowicz, Czeslaw Bylinski — 2004
A Declarative Language for the Coq Proof AssistantP. Corbineau — 2007
A Brief Overview of MizarAdam Naumowicz, Artur Korniłowicz — 2009
Information Retrieval in MMLG. Bancerek, P. Rudnicki — 2003
XML-izing Mizar: Making Semantic Processing and Presentation of MML EasyJ. Urban — 2005
A Mizar Mode for HOLJ. Harrison — 1996

Cited by

New Developments in Parsing MizarJesse Alama, Lionel Mamane, Josef Urban — 2011
The development of argument and computation and its roots in the LVOV-Warsaw schoolChris Reed, Marcin Koszowy — 2011
Machine Learning for Automated ReasoningDaniel Kühlwein — 2014
Definitional Expansions in MizarArtur Korniłowicz — 2015
Improving Legibility of Formal Proofs Based on the Close Reference Principle is NP-HardKarol Pąk — 2015
Towards automatically categorizing mathematical knowledgeAdam Grabowski, Christoph Schwarzweller — 2012
Automated Discovery of Properties of Rough SetsAdam Grabowski — 2013
T2Ku: Building a Semantic Wiki of MathematicsMinqi Pan — 2012
On the computer certification of fuzzy numbersAdam Grabowski — 2013
Flexary connectives in MizarArtur Korniłowicz — 2015
Eliciting Implicit Assumptions of Mizar Proofs by Property OmissionJesse Alama — 2011
Sentence complexity of theorems in MizarJesse Alama — 2013
MizAR 40 for Mizar 40Cezary Kaliszyk, Josef Urban — 2013
Efficient Semantic Features for Automated Reasoning over Large TheoriesCezary Kaliszyk, Josef Urban, J Vyskočil — 2015
Equality in computer proof-assistantsAdam Grabowski, Artur Korniłowicz, Christoph Schwarzweller — 2015
Efficient Rough Set Theory MergingAdam Grabowski — 2014
Machine Learning in Proof General: Interfacing InterfacesEkaterina Komendantskaya, Jónathan Heras, Gudmund Grov — 2012
Premise Selection for Mathematics by Corpus Analysis and Kernel MethodsJesse Alama, Tom Heskes, Daniel Kühlwein — 2011
Improving legibility of natural deduction proofs is not trivialKarol Pąk — 2014
Custom Automations in MizarMarco B. Caminati, Giuseppe Rosolini — 2013

Related papers

MPTP 0.2: Design, Implementation, and Initial ExperimentsJosef Urban — 2006
Premise Selection for Mathematics by Corpus Analysis and Kernel MethodsJesse Alama, Tom Heskes, Daniel Kühlwein — 2011
MizAR 40 for Mizar 40Cezary Kaliszyk, Josef Urban — 2013
E – a brainiac theorem proverStephan Schulz — 2002
Learning-Assisted Automated Reasoning with FlyspeckCezary Kaliszyk, Josef Urban — 2012
ATP and Presentation Service for Mizar FormalizationsJosef Urban, Piotr Rudnicki, Geoff Sutcliffe — 2011
Methods of Lemma Extraction in Natural Deduction ProofsKarol Pąk — 2012