Avoiding duplications in tableau systems for intuitionistic logic and Kuroda logic

DOI10.1093/jigpal/5.1.145zbMath0874.03009OpenAlexW2094946156MaRDI QIDQ4340932

Mario Ornaghi, Pierangelo Miglioli, Ugo Moscato

Publication date: 5 November 1997

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

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

zbMATH Keywords

intuitionistic logictableau systemsproof searchKuroda 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)

Related Items (7)

KALC: a constructive semantics for ALC ⋮ An Evaluation-Driven Decision Procedure for G3i ⋮ Generalized tableau systems for intermediate propositional logics ⋮ Admissibility of structural rules for contraction-free systems of intuitionistic logic ⋮ Optimization techniques for propositional intuitionistic logic and their implementation ⋮ A tableau calculus for Propositional Intuitionistic Logic with a refined treatment of nested implications ⋮ Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models

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