Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic

DOI10.1007/978-3-319-41579-6_24zbMath1461.68248OpenAlexW2479250907MaRDI QIDQ3179185

Bruno Woltzenlogel Paleo

Publication date: 21 December 2016

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-41579-6_24

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Proof theory in general (including proof-theoretic semantics) (03F03) Paraconsistent logics (03B53) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Sledgehammer
• Skeptik

Cites Work

• Unnamed Item
• Resolution proof transformation for compression and interpolation
• Compression of Propositional Resolution Proofs by Lowering Subproofs
• Towards Algorithmic Cut-Introduction
• On the proof complexity of deep inference
• Reducing redundancy in cut-elimination by resolution
• A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
• Atomic Cut Introduction by Resolution: Proof Structuring and Compression
• Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses
• Contextual Natural Deduction
• Two Techniques for Minimizing Resolution Proofs
• Compression of Propositional Resolution Proofs via Partial Regularization
• Computer Science Logic
• A Local System for Intuitionistic Logic
• Herbrand Sequent Extraction
• An Algorithmic Interpretation of a Deep Inference System
• Sledgehammer: Judgement Day

This page was built for publication: Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic