Methods of lemma extraction in natural deduction proofs

DOI10.1007/S10817-012-9267-0zbMath1260.68379OpenAlexW2060832326WikidataQ124791874 ScholiaQ124791874MaRDI QIDQ1945902

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)

Related Items (14)

Four decades of {\textsc{Mizar}}. Foreword ⋮ 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 ⋮ Readable Formalization of Euler’s Partition Theorem in Mizar ⋮ Mizar: State-of-the-art and Beyond ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ Formalizing Lattice-Theoretical Aspects of Rough and Fuzzy Sets ⋮ Initial Comparison of Formal Approaches to Fuzzy and Rough Sets ⋮ Accessing the Mizar Library with a Weakly Strict Mizar Parser ⋮ Automated Improving of Proof Legibility in the Mizar System ⋮ SAT-Enhanced Mizar Proof Checking

Uses Software

• Mizar

Cites Work

• Unnamed Item
• Unnamed Item
• Tentative Experiments with Ellipsis in Mizar
• Mathematical Knowledge Management

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