Accessing the Mizar Library with a Weakly Strict Mizar Parser
From MaRDI portal
Publication:2817295
DOI10.1007/978-3-319-42547-4_6zbMath1344.68211OpenAlexW2504382997MaRDI QIDQ2817295
Radosław Piliszek, Adam Naumowicz
Publication date: 30 August 2016
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-42547-4_6
Related Items
A new export of the Mizar mathematical library ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Semantics of Mizar as an Isabelle object logic
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- 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
- Flexary connectives in Mizar
- A comparison of Mizar and Isar
- Methods of lemma extraction in natural deduction proofs
- On rewriting rules in Mizar
- Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13--17, 2015, Proceedings
- New Developments in Parsing Mizar
- Improving legibility of natural deduction proofs is not trivial
- Readable Formalization of Euler’s Partition Theorem in Mizar
- Mizar: State-of-the-art and Beyond
- Tools for MML Environment Analysis
- On Duplication in Mathematical Repositories
- Licensing the Mizar Mathematical Library
- mizar-items: Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
- Efficient Rough Set Theory Merging
- Automated Discovery of Properties of Rough Sets
- Revisions as an Essential Tool to Maintain Mathematical Repositories
- Interfacing external CA systems for Gröbner bases computation in M<scp>izar</scp>proof checking
- Mathematical Knowledge Management
