A Brief Overview of Mizar

DOI10.1007/978-3-642-03359-9_5zbMath1252.68262OpenAlexW1530333737WikidataQ56168712 ScholiaQ56168712MaRDI QIDQ3183518

Adam Naumowicz, Artur Korniłowicz

Publication date: 20 October 2009

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-03359-9_5

Mathematics Subject Classification ID

Related Items

Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs, Four decades of {\textsc{Mizar}}. Foreword, Mechanizing complemented lattices within Mizar type system, Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization, Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver, Improving legibility of formal proofs based on the close reference principle is NP-hard, Mizar: State-of-the-art and Beyond, Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library, Tools for MML Environment Analysis, CoSMed: a confidentiality-verified social media platform, Characteristics of de Bruijn’s early proof checker Automath, What is the point of computers? A question for pure mathematicians, Random Forests for Premise Selection, On rewriting rules in Mizar, Formalization of real analysis: a survey of proof assistants and libraries, Formalizing Lattice-Theoretical Aspects of Rough and Fuzzy Sets, Flexary connectives in Mizar, Proof verification and proof discovery for relativity, Coquelicot: a user-friendly library of real analysis for Coq, Initial Comparison of Formal Approaches to Fuzzy and Rough Sets, Mizar, Arithmetic operations on short finite sequences, The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider’s “Logical Approach to Discrete Math”, Semantics of Mizar as an Isabelle object logic, Mechanized metatheory revisited, Automated Improving of Proof Legibility in the Mizar System, SAT-Enhanced Mizar Proof Checking

Uses Software

• Coq
• Isar
• HOL Light
• MML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A comparison of Mizar and Isar
• A Declarative Language for the Coq Proof Assistant
• On a Practical Way of Describing Formal Deductions
• Mathematical Knowledge Management
• Mizar Course in Logic and Set Theory
• Types for Proofs and Programs
• Mathematical Knowledge Management