Sequent Calculus for Intuitionistic Epistemic Logic IEL

DOI10.1007/978-3-319-27683-0_14MaRDI QIDQ5283428zbMATH OpenOpenAlexFDO

Authors Alexey Yatmanov, Vladimir Nikolaevich Krupskiĭ

Publication date 21 July 2017

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

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

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)

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.

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

Cites work

• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• scientific article; zbMATH DE number 795590 (Why is no real title available?)
• scientific article; zbMATH DE number 3073037 (Why is no real title available?)
• Alternation
• INTUITIONISTIC EPISTEMIC LOGIC
• Intuitionistic propositional logic is polynomial-space complete
• On intuitionistic modal epistemic logic
• The Church-Fitch knowability paradox in the light of structural proof theory
• Typing in reflective combinatory logic

Cited in

(13)

• Semantics for intuitionistic epistemic logics of shallow depths for game theory
• Sequent calculi for intuitionistic Gödel-Löb logic
• Cut-free and analytic sequent calculus of intuitionistic epistemic logic
• Reasoning about proof and knowledge
• Cut elimination and complexity bounds for intuitionistic epistemic logic
• Constructive knowledge and the justified true belief paradigm
• INTUITIONISTIC EPISTEMIC LOGIC
• Modal type theory based on the intuitionistic modal logic \(\mathrm{IEL}^{-}\)
• Linear depth deduction with subformula property for intuitionistic epistemic logic
• Axiomatizing epistemic logic of friendship via tree sequent calculus
• A first-order expansion of Artemov and Protopopescu's intuitionistic epistemic logic
• A labelled sequent calculus for intuitionistic public announcement logic
• On Artemov and Protopopescu's intuitionistic epistemic logic expanded with distributed knowledge

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)