Proof-Search in Natural Deduction Calculus for Classical Propositional Logic

DOI10.1007/978-3-319-24312-2_17MaRDI QIDQ3455774zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Proof-search of propositional intuitionistic logic sequents by means of classical logic calculus
• scientific article; zbMATH DE number 1390270
• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• A proof-search procedure for intuitionistic propositional logic
• Proof-finding algorithms for classical and subclassical propositional logics
• scientific article; zbMATH DE number 1354109
• scientific article; zbMATH DE number 1348467
• Natural deduction for non-classical logics
• Proof search in natural deduction systems for negative syllogistics
• Probabilized Sequent Calculus and Natural Deduction System for Classical Logic

Cites work

• scientific article; zbMATH DE number 1809865 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• A Terminating Evaluation-Driven Variant of G3i
• An evaluation-driven decision procedure for G3i
• Classical natural deduction
• Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
• Focusing and polarization in linear, intuitionistic, and classical logics
• Goal-directed proof theory
• Mechanizing Mathematical Reasoning
• Natural deduction, hybrid systems and modal logics
• Normal natural deduction proofs (in classical logic)

Cited in

(14)

• On the intuitionistic force of classical search (extended abstract)
• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• Normality, non-contamination and logical depth in classical natural deduction
• The polarized \(\lambda\)-calculus
• On multiple conclusion deductions in classical logic
• A Compressing Translation from Propositional Resolution to Natural Deduction
• ADC method of proof search for intuitionistic propositional natural deduction
• Implementation and evaluation of contextual natural deduction for minimal logic
• Correspondence analysis and automated proof-searching for first degree entailment
• Natural deduction in a paracomplete setting
• Mechanizing Mathematical Reasoning
• scientific article; zbMATH DE number 221557 (Why is no real title available?)
• Correspondence analysis for some fragments of classical propositional logic
• scientific article; zbMATH DE number 7599926 (Why is no real title available?)

Describes a project that uses

Uses Software

• MUSCADET

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3455774)