Improving legibility of natural deduction proofs is not trivial
From MaRDI portal
Publication:2921120
DOI10.2168/LMCS-10(3:23)2014zbMath1341.68196arXiv1407.1140OpenAlexW1996197605MaRDI QIDQ2921120
Publication date: 30 September 2014
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1407.1140
Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Methodology of mathematics (00A35)
Related Items
Mechanizing complemented lattices within Mizar type system, Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization, Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver, Improving legibility of formal proofs based on the close reference principle is NP-hard, Semi-intelligible Isar proofs from machine-generated proofs, Mizar: State-of-the-art and Beyond, Accessing the Mizar Library with a Weakly Strict Mizar Parser, Multiplication-related classes of complex numbers
Uses Software
