Sequent Calculus for Intuitionistic Epistemic Logic IEL

DOI10.1007/978-3-319-27683-0_14zbMATH Open1476.03014arXiv1508.07851OpenAlexW2201994833MaRDI QIDQ5283428FDOQ5283428

Alexey Yatmanov, Vladimir Nikolaevich Krupskiĭ

Publication date: 21 July 2017

Published in: Logical Foundations of Computer Science (Search for Journal in Brave)

Abstract: The formal system of intuitionistic epistemic logic IEL was proposed by S. Artemov and T. Protopopescu. It provides the formal foundation for the study of knowledge from an intuitionistic point of view based on Brouwer-Hayting-Kolmogorov semantics of intuitionism. We construct a cut-free sequent calculus for IEL and establish that polynomial space is sufficient for the proof search in it. So, we prove that IEL is PSPACE-complete.

Full work available at URL: https://arxiv.org/abs/1508.07851

Recommendations

• scientific article; zbMATH DE number 218517
• Cut-free and analytic sequent calculus of intuitionistic epistemic logic
• Sequent calculi for default and autoepistemic logics
• Gentzen-style sequent calculus for semi-intuitionistic logic
• Sequent calculi for intuitionistic Gödel-Löb logic
• On sequent calculi for intuitionistic propositional logic.
• Labelled sequent calculus for inquisitive logic
• Intuitionistic sequent calculi for finitely many-valued logics
• scientific article; zbMATH DE number 1390272
• Natural deduction and sequent calculus for intuitionistic relevant logic

zbMATH Keywords

modal logicsequent calculuscut-eliminationPSPACEintuitionistic epistemic logic

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Logics of knowledge and belief (including belief change) (03B42) Cut-elimination and normal-form theorems (03F05) Subsystems of classical logic (including intuitionistic logic) (03B20)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Alternation
• Title not available (Why is that?)
• On intuitionistic modal epistemic logic
• The Church-Fitch knowability paradox in the light of structural proof theory
• Intuitionistic propositional logic is polynomial-space complete
• INTUITIONISTIC EPISTEMIC LOGIC
• Typing in reflective combinatory logic

Cited In (5)

• INTUITIONISTIC EPISTEMIC LOGIC
• A first-order expansion of Artemov and Protopopescu's intuitionistic epistemic logic
• Linear depth deduction with subformula property for intuitionistic epistemic logic
• On Artemov and Protopopescu's intuitionistic epistemic logic expanded with distributed knowledge
• Constructive knowledge and the justified true belief paradigm

This page was built for publication: Sequent Calculus for Intuitionistic Epistemic Logic IEL

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