Simplification Rules for Intuitionistic Propositional Tableaux

DOI10.1145/2159531.2159536MaRDI QIDQ2946662zbMATH OpenOpenAlexFDO

Authors Mauro Ferrari, Camillo Fiorentini, Guido Fiorino

Publication date 17 September 2015

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2434/204038

zbMATH Keywords

decision proceduresintuitionistic logicsimplification rulestableau calculi

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1189106
• Tableaux for intuitionistic logics
• A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications
• Almost duplication-free tableau calculi for propositional lax logics
• scientific article; zbMATH DE number 2024622
• Generalized tableau systems for intermediate propositional logics
• A tableaux calculus for default intuitionistic logic
• scientific article; zbMATH DE number 2080337
• Simplified tableaux for STIT imagination logic
• scientific article; zbMATH DE number 1292293

Cited in

(14)

• Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
• Efficient SAT-based proof search in intuitionistic propositional logic
• A non-clausal tableau calculus for \textsc{MinSat}
• An evaluation-driven decision procedure for G3i
• Intuitionistic Decision Procedures Since Gentzen
• Tree trimming: four non-branching rules for Priest's \textit{Introduction to non-classical logic}
• Clausal intuitionistic logic II. tableau proof procedures
• scientific article; zbMATH DE number 1189106 (Why is no real title available?)
• An O(n log n)-Space Decision Procedure for Intuitionistic Propositional Logic
• Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic
• Simplifying and generalizing formulae in tableaux. Pruning the search space and building models
• scientific article; zbMATH DE number 5199142 (Why is no real title available?)
• General clauses for SAT-based proof search in intuitionistic propositional logic
• Optimization techniques for propositional intuitionistic logic and their implementation

This page was built for publication: Simplification Rules for Intuitionistic Propositional Tableaux

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