Methods of lemma extraction in natural deduction proofs

DOI10.1007/S10817-012-9267-0zbMATH Open1260.68379OpenAlexW2060832326WikidataQ124791874 ScholiaQ124791874MaRDI QIDQ1945902FDOQ1945902

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

Recommendations

• scientific article
• 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

zbMATH Keywords

natural deductionlegibilitylemma extraction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Title not available (Why is that?)
• Tentative experiments with ellipsis in Mizar
• Title not available (Why is that?)
• Mathematical Knowledge Management

Cited In (16)

• 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
• Automated Improving of Proof Legibility in the Mizar System
• Readable formalization of Euler's partition theorem in Mizar
• The role of the Mizar mathematical library for interactive proof development in Mizar
• Accessing the Mizar library with a weakly strict Mizar parser
• SAT-enhanced Mizar proof checking
• Four decades of \textsc{Mizar}. Foreword
• Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver
• Formalizing lattice-theoretical aspects of rough and fuzzy sets
• Extracting Information from Logical Proofs
• Initial comparison of formal approaches to fuzzy and rough sets
• Improving legibility of natural deduction proofs is not trivial
• Mizar: state-of-the-art and beyond

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)