Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
From MaRDI portal
Publication:286801
DOI10.1007/s10817-015-9331-7zbMath1356.68192OpenAlexW826005707WikidataQ59407724 ScholiaQ59407724MaRDI QIDQ286801
Publication date: 26 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-015-9331-7
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (4)
The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Extending numeric automation for number theory formalizations in Mizar ⋮ Accessing the Mizar Library with a Weakly Strict Mizar Parser ⋮ Enhancement of Mizar Texts with Transitivity Property of Predicates
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Gazing: An approach to the problem of definition and lemma use
- On the rules of suppositions in formal logic
- Methods of lemma extraction in natural deduction proofs
- The Mizar Mathematical Library in OMDoc: translation and applications
- On rewriting rules in Mizar
- New Developments in Parsing Mizar
- Improving legibility of natural deduction proofs is not trivial
- A Brief Overview of Mizar
- Licensing the Mizar Mathematical Library
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Revisions as an Essential Tool to Maintain Mathematical Repositories
- SAT-Enhanced Mizar Proof Checking
- Evaluation of Automated Theorem Proving on the Mizar Mathematical Library
- Information Retrieval and Rendering with MML Query
- Interfacing external CA systems for Gröbner bases computation in M<scp>izar</scp>proof checking
- Mathematical Knowledge Management
- Mathematical Knowledge Management
This page was built for publication: Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
