Proof-Search in Natural Deduction Calculus for Classical Propositional Logic

DOI10.1007/978-3-319-24312-2_17zbMath1471.68308OpenAlexW2255911289MaRDI 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

Mathematics Subject Classification ID

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

Related Items (6)

Correspondence analysis for some fragments of classical propositional logic ⋮ Correspondence analysis and automated proof-searching for first degree entailment ⋮ Goal-oriented proof-search in natural deduction for intuitionistic propositional logic ⋮ The polarized \(\lambda\)-calculus ⋮ Unnamed Item ⋮ Normality, non-contamination and logical depth in classical natural deduction

Uses Software

• MUSCADET

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: Proof-Search in Natural Deduction Calculus for Classical Propositional Logic