Proof-Search in Natural Deduction Calculus for Classical Propositional Logic
From MaRDI portal
Publication:3455774
DOI10.1007/978-3-319-24312-2_17zbMath1471.68308MaRDI QIDQ3455774
Mauro Ferrari, Camillo Fiorentini
Publication date: 11 December 2015
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-24312-2_17
03B35: Mechanization of proofs and logical operations
03B05: Classical propositional logic
03F03: Proof theory in general (including proof-theoretic semantics)
68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
Uses Software
Cites Work
- Natural deduction, hybrid systems and modal logics
- Focusing and polarization in linear, intuitionistic, and classical logics
- Normal natural deduction proofs (in classical logic)
- Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
- A Terminating Evaluation-Driven Variant of G3i
- An Evaluation-Driven Decision Procedure for G3i
- Mechanizing Mathematical Reasoning
- Goal-directed proof theory
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item