A Brief Overview of Mizar
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1951634 (Why is no real title available?)
- scientific article; zbMATH DE number 1863397 (Why is no real title available?)
- scientific article; zbMATH DE number 1424018 (Why is no real title available?)
- scientific article; zbMATH DE number 3076631 (Why is no real title available?)
- A Declarative Language for the Coq Proof Assistant
- A comparison of Mizar and Isar
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Mizar Course in Logic and Set Theory
- On a Practical Way of Describing Formal Deductions
- Types for Proofs and Programs
Cited in
(36)- Characteristics of de Bruijn’s early proof checker Automath
- Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
- Mechanizing complemented lattices within Mizar type system
- Mechanized metatheory revisited
- Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
- Improving legibility of formal proofs based on the close reference principle is NP-hard
- The teaching tool CalcCheck: a proof-checker for Gries and Schneider's ``Logical approach to discrete math
- Random forests for premise selection
- Automated Improving of Proof Legibility in the Mizar System
- Mizar
- CoSMed: a confidentiality-verified social media platform
- scientific article; zbMATH DE number 5850143 (Why is no real title available?)
- Implementation of the composition-nominative approach to program formalization in Mizar
- Teaching semantics with a proof assistant: no more LSD trip proofs
- Accessing the Mizar library with a weakly strict Mizar parser
- Flexary connectives in Mizar
- Four decades of \textsc{Mizar}. Foreword
- Tentative experiments with ellipsis in Mizar
- Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
- Mechanized HOL reasoning in set theory
- SAT-enhanced Mizar proof checking
- On rewriting rules in Mizar
- Formalizing lattice-theoretical aspects of rough and fuzzy sets
- Formalization of real analysis: a survey of proof assistants and libraries
- Alternative Aggregates in Mizar
- Initial comparison of formal approaches to fuzzy and rough sets
- Semantics of Mizar as an Isabelle object logic
- Arithmetic operations on short finite sequences
- Mizar: state-of-the-art and beyond
- Tools for MML environment analysis
- Equivalence checking for orthocomplemented bisemilattices in log-linear time
- Formula normalizations in verification
- Proof verification and proof discovery for relativity
- Smm, the simplified metamath
- Coquelicot: a user-friendly library of real analysis for Coq
- What is the point of computers? A question for pure mathematicians
This page was built for publication: A Brief Overview of Mizar
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3183518)
