zbMATH — the first resource for mathematics

Sequent calculus for intuitionistic epistemic logic IEL. (English) Zbl 06751239
Artemov, Sergei (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2016, Deerfield Beach, FL, USA, January 4–7, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9537, 187-201 (2016).
Summary: 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. We prove that IEL is PSPACE-complete.
For the entire collection see [Zbl 1364.03006].

03B70 Logic in computer science
Full Text: DOI
[1] Artemov, S., Protopopescu, T.: Intuitionistic Epistemic Logic (2014). arXiv:1406.1582v2 · Zbl 1408.03004
[2] Williamson, T.: On intuitionistic modal epistemic logic. J. Philos. Log. 21(1), 63–89 (1992) · Zbl 0746.03014
[3] Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. The MIT Press, Cambridge (1995) · Zbl 0839.68095
[4] Maffezioli, V., Naibo, A., Negri, S.: The Church-Fitch knowability paradox in the light of structural proof theory. Synthese 190, 2677–2716 (2013) · Zbl 1284.03071
[5] Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (1996) · Zbl 0868.03024
[6] Kleene, S.C.: Introduction to Metamathematics. North-Holland Publ. Co., Amsterdam (1952) · Zbl 0047.00703
[7] Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. Assoc. Comput. Mach. 28, 114–133 (1981) · Zbl 0473.68043
[8] Statman, R.: Intuitionistic propositional logic is polynomial-space complete. Theor. Comput. Sci. 9, 67–72 (1979) · Zbl 0411.03049
[9] Krupski, V.N.: Introduction to Computational Complexity. Factorial Press, Moscow (2006). (In Russian)
[10] Kitaev, A., Shen, A., Vyalyi, M.: Classical and Quantum Computations. MCCME-CheRo, Moscow (1999). (In Russian)
[11] Krupski, N.: Typing in reflective combinatory logic. Ann. Pure Appl. Log. 141, 243–256 (2006) · Zbl 1103.03016
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.