Sequent Calculus for Intuitionistic Epistemic Logic IEL

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

Authors: 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 (13)

• Cut elimination and complexity bounds for intuitionistic epistemic logic
• 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
• Reasoning about proof and knowledge
• Cut-free and analytic sequent calculus of intuitionistic epistemic logic
• On Artemov and Protopopescu's intuitionistic epistemic logic expanded with distributed knowledge
• Semantics for intuitionistic epistemic logics of shallow depths for game theory
• Sequent calculi for intuitionistic Gödel-Löb logic
• Axiomatizing epistemic logic of friendship via tree sequent calculus
• Modal type theory based on the intuitionistic modal logic \(\mathrm{IEL}^{-}\)
• Constructive knowledge and the justified true belief paradigm
• A labelled sequent calculus for intuitionistic public announcement logic

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)