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
