Improving legibility of formal proofs based on the close reference principle is NP-hard
From MaRDI portal
Publication:286805
DOI10.1007/s10817-015-9337-1zbMath1356.68198OpenAlexW1268136390WikidataQ59407604 ScholiaQ59407604MaRDI QIDQ286805
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-9337-1
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (6)
Presentation and manipulation of Mizar properties in an Isabelle object logic ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Computer Certification of Generalized Rough Sets Based on Relations ⋮ Accessing the Mizar Library with a Weakly Strict Mizar Parser ⋮ Enhancement of Mizar Texts with Transitivity Property of Predicates ⋮ Taxonomies of geometric problems
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Methods of lemma extraction in natural deduction proofs
- On rewriting rules in Mizar
- Tentative Experiments with Ellipsis in Mizar
- Improving legibility of natural deduction proofs is not trivial
- A Brief Overview of Mizar
- A Declarative Language for the Coq Proof Assistant
- Licensing the Mizar Mathematical Library
- Efficient Rough Set Theory Merging
- Mathematical Knowledge Management
- 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
- Mathematical Knowledge Management
This page was built for publication: Improving legibility of formal proofs based on the close reference principle is NP-hard
