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

DOI10.3166/JANCL.19.149-166zbMath1187.03011OpenAlexW2049227737MaRDI QIDQ3647294

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

intuitionistic propositional logictableau calculidecision procedures

Mathematics Subject Classification ID

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

Related Items

An Evaluation-Driven Decision Procedure for G3i ⋮ A tableaux calculus for default intuitionistic logic ⋮ Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models

Uses Software

• STRIP

Cites Work

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

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