Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization

DOI10.1007/S10817-015-9331-7zbMath1356.68192OpenAlexW826005707WikidataQ59407724 ScholiaQ59407724MaRDI QIDQ286801

Artur Korniłowicz

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

zbMATH Keywords

formal verificationproof assistantMizardefinitional expansion

Mathematics Subject Classification ID

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

• Mizar
• MML
• OMDoc

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