Improving legibility of formal proofs based on the close reference principle is NP-hard
DOI10.1007/S10817-015-9337-1zbMATH Open1356.68198OpenAlexW1268136390WikidataQ59407604 ScholiaQ59407604MaRDI QIDQ286805FDOQ286805
Authors: Karol Pąk 
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
Recommendations
Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mechanization of proofs and logical operations (03B35)
Cites Work
- Title not available (Why is that?)
- A Brief Overview of Mizar
- Title not available (Why is that?)
- Efficient rough set theory merging
- 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 Declarative Language for the Coq Proof Assistant
- Title not available (Why is that?)
- Title not available (Why is that?)
- Licensing the Mizar Mathematical Library (MML)
- Formal proof - the four color theorem
- 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 Mizar proof checking
- Mathematical Knowledge Management
- Mathematical Knowledge Management
Cited In (8)
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- Taxonomies of geometric problems
- Computer certification of generalized rough sets based on relations
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Accessing the Mizar library with a weakly strict Mizar parser
- Enhancement of \textsc{Mizar} texts with transitivity property of predicates
- Methods of lemma extraction in natural deduction proofs
- Improving legibility of natural deduction proofs is not trivial
Uses Software
This page was built for publication: Improving legibility of formal proofs based on the close reference principle is NP-hard
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q286805)
