Implementation and Evaluation of Contextual Natural Deduction for Minimal Logic
From MaRDI portal
Publication:3179185
DOI10.1007/978-3-319-41579-6_24zbMath1461.68248OpenAlexW2479250907MaRDI QIDQ3179185
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
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
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