A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications

DOI10.3166/JANCL.19.149-166MaRDI QIDQ3647294zbMATH OpenOpenAlexFDO

Authors Mauro Ferrari, Camillo Fiorentini, Guido Fiorino

Publication date 30 November 2009

Published in Journal of Applied Non-Classical Logics (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3166/jancl.19.149-166

zbMATH Keywords

tableau calculidecision proceduresintuitionistic propositional logic

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Mechanization of proofs and logical operations (03B35)

Recommendations

• A tableaux calculus for default intuitionistic logic
• Tableaux for intuitionistic logics
• scientific article; zbMATH DE number 1361525
• scientific article; zbMATH DE number 2090533
• Fibred tableaux for multi-implication logics
• scientific article; zbMATH DE number 1390272
• Clausal intuitionistic logic II. tableau proof procedures
• Cut-free tableau calculi for some intuitionistic modal logics
• scientific article; zbMATH DE number 1292293
• On deriving nested calculi for intuitionistic logics from semantic systems

Cites work

• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic
• Bounds for cut elimination in intuitionistic propositional logic
• Contraction-free sequent calculi for intuitionistic logic
• Intuitionistic propositional logic is polynomial-space complete
• Optimization techniques for propositional intuitionistic logic and their implementation
• Space-efficient Decision Procedures for Three Interpolable Propositional Intermediate Logics
• The ILTP problem library for intuitionistic logic

Cited in

(14)

• A tableaux calculus for default intuitionistic logic
• Improvements to the Tableau Prover PITP
• scientific article; zbMATH DE number 5592264 (Why is no real title available?)
• A Tableau Calculus for Hajek's Logic BL
• scientific article; zbMATH DE number 1361525 (Why is no real title available?)
• Space-efficient Decision Procedures for Three Interpolable Propositional Intermediate Logics
• An evaluation-driven decision procedure for G3i
• Simplification Rules for Intuitionistic Propositional Tableaux
• scientific article; zbMATH DE number 1612548 (Why is no real title available?)
• scientific article; zbMATH DE number 1390272 (Why is no real title available?)
• Tableaux for intuitionistic logics
• Computer Science Logic
• Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
• scientific article; zbMATH DE number 2024622 (Why is no real title available?)

Describes a project that uses

Uses Software

• STRIP

This page was built for publication: A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications

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