Improving legibility of formal proofs based on the close reference principle is NP-hard
From MaRDI portal
(Redirected from Publication:286805)
Recommendations
Cites work
- A Brief Overview of Mizar
- A Declarative Language for the Coq Proof Assistant
- Automated Discovery of Properties of Rough Sets
- Efficient rough set theory merging
- Formal proof - the four color theorem
- scientific article; zbMATH DE number 5850143 (Why is no real title available?)
- scientific article; zbMATH DE number 3639144 (Why is no real title available?)
- scientific article; zbMATH DE number 1863397 (Why is no real title available?)
- scientific article; zbMATH DE number 1424018 (Why is no real title available?)
- Improving legibility of natural deduction proofs is not trivial
- Interfacing external CA systems for Gröbner bases computation in Mizar proof checking
- Licensing the Mizar Mathematical Library (MML)
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Mathematical Knowledge Management
- Methods of lemma extraction in natural deduction proofs
- On rewriting rules in Mizar
- Revisions as an Essential Tool to Maintain Mathematical Repositories
- Tentative experiments with ellipsis in Mizar
Cited in
(8)- The role of the Mizar mathematical library for interactive proof development in Mizar
- Methods of lemma extraction in natural deduction proofs
- Taxonomies of geometric problems
- Presentation and manipulation of Mizar properties in an Isabelle object logic
- Accessing the Mizar library with a weakly strict Mizar parser
- Enhancement of \textsc{Mizar} texts with transitivity property of predicates
- Improving legibility of natural deduction proofs is not trivial
- Computer certification of generalized rough sets based on relations
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)
