Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic

DOI10.1093/JIGPAL/5.1.145MaRDI QIDQ4340932zbMATH OpenOpenAlexFDO

Authors Pierangelo Miglioli, Ugo Moscato, Mario Ornaghi

Publication date 5 November 1997

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/jigpal/5.1.145

zbMATH Keywords

intuitionistic logicproof searchtableau systemsKuroda logicduplication of formulas

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20) Intermediate logics (03B55)

Recommendations

• An improved refutation system for intuitionistic predicate logic
• Simplification Rules for Intuitionistic Propositional Tableaux
• Generalized tableau systems for intermediate propositional logics
• Duplication-free tableau calculi and related cut-free sequent calculi for the interpolable propositional intermediate logics

Cited in

(9)

• Admissibility of structural rules for contraction-free systems of intuitionistic logic
• A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications
• \({\mathcal KALC}\): a constructive semantics for \({\mathcal ALC}\)
• An evaluation-driven decision procedure for G3i
• Generalized tableau systems for intermediate propositional logics
• An improved refutation system for intuitionistic predicate logic
• Optimization techniques for propositional intuitionistic logic and their implementation
• Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models
• scientific article; zbMATH DE number 5661162 (Why is no real title available?)

This page was built for publication: Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic

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