Methods of lemma extraction in natural deduction proofs

DOI10.1007/S10817-012-9267-0MaRDI QIDQ1945902zbMATHOpenAlexWikidataFDO

Authors Karol Pąk

Publication date 17 April 2013

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-012-9267-0

zbMATH Keywords

natural deductionlegibilitylemma extraction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 4164180
• Improving legibility of natural deduction proofs is not trivial
• Presenting intuitive deductions via symmetric simplification
• Improving legibility of formal proofs based on the close reference principle is NP-hard
• On the generation of quantified lemmas

Cites work

• scientific article; zbMATH DE number 5850143 (Why is no real title available?)
• scientific article; zbMATH DE number 1951637 (Why is no real title available?)
• Mathematical Knowledge Management
• Tentative experiments with ellipsis in Mizar

Cited in

(16)

• The role of the Mizar mathematical library for interactive proof development in Mizar
• Formalizing lattice-theoretical aspects of rough and fuzzy sets
• Mechanizing complemented lattices within Mizar type system
• Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
• Improving legibility of formal proofs based on the close reference principle is NP-hard
• Semi-intelligible Isar proofs from machine-generated proofs
• SAT-enhanced Mizar proof checking
• Initial comparison of formal approaches to fuzzy and rough sets
• Automated Improving of Proof Legibility in the Mizar System
• Accessing the Mizar library with a weakly strict Mizar parser
• Four decades of \textsc{Mizar}. Foreword
• Improving legibility of natural deduction proofs is not trivial
• Mizar: state-of-the-art and beyond
• Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
• Extracting Information from Logical Proofs
• Readable formalization of Euler's partition theorem in Mizar

Describes a project that uses

Uses Software

• Mizar

This page was built for publication: Methods of lemma extraction in natural deduction proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1945902)