{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,25]],"date-time":"2025-09-25T14:44:55Z","timestamp":1758811495670},"reference-count":13,"publisher":"Oxford University Press (OUP)","issue":"1","license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,1,23]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>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\u2013Heyting\u2013Kolmogorov 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.<\/jats:p>","DOI":"10.1093\/logcom\/exaa012","type":"journal-article","created":{"date-parts":[[2020,1,6]],"date-time":"2020-01-06T12:08:28Z","timestamp":1578312508000},"page":"281-294","source":"Crossref","is-referenced-by-count":3,"title":["Cut elimination and complexity bounds for intuitionistic epistemic logic"],"prefix":"10.1093","volume":"30","author":[{"given":"Vladimir N","family":"Krupski","sequence":"first","affiliation":[{"name":"Faculty of Mechanics and Mathematics, Lomonosov Moscow State University, Moscow 119991, Russia"}]}],"member":"286","published-online":{"date-parts":[[2020,2,20]]},"reference":[{"key":"2020040702351779700_ref1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2687821","article-title":"Explicit provability and constructive semantics","volume":"7,","author":"Artemov","year":"2001","journal-title":"Bulletin of Symbolic Logic,"},{"key":"2020040702351779700_ref2","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1017\/S1755020315000374","article-title":"Intuitionistic epistemic logic","volume":"9,","author":"Artemov","year":"2016","journal-title":"The Review of Symbolic Logic,"},{"key":"2020040702351779700_ref3","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/322234.322243","article-title":"Alternation","volume":"28","author":"Chandra","year":"1981","journal-title":"Journal of the Association for Computing Machinery"},{"key":"2020040702351779700_ref4","volume-title":"Reasoning about Knowledge","author":"Fagin","year":"1995"},{"key":"2020040702351779700_ref5","volume-title":"Classical and Quantum Computations","author":"Kitaev","year":"1999"},{"key":"2020040702351779700_ref6","volume-title":"Introduction to Metamathematics","author":"Kleene","year":"1952"},{"key":"2020040702351779700_ref7","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/j.apal.2005.11.004","article-title":"Typing in reflective combinatory logic","volume":"141","author":"Krupski","year":"2006","journal-title":"Annals of Pure and Applied Logic"},{"key":"2020040702351779700_ref8","volume-title":"Introduction to Computational Complexity","author":"Krupski","year":"2006"},{"key":"2020040702351779700_ref9","doi-asserted-by":"crossref","first-page":"2677","DOI":"10.1007\/s11229-012-0061-7","article-title":"The Church-Fitch knowability paradox in the light of structural proof theory","volume":"190","author":"Maffezioli","year":"2013","journal-title":"Synthese"},{"key":"2020040702351779700_ref10","first-page":"317","article-title":"An arithmetical interpretation of verification and intuitionistic knowledge","volume-title":"Logical Foundations of Computer Science, LFCS 2016, Lecture Notes in Computer Science 9537","author":"Protopopescu","year":"2016"},{"key":"2020040702351779700_ref11","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(79)90006-9","article-title":"Intuitionistic propositional logic is polynomial-space complete","volume":"9","author":"Statman","year":"1979","journal-title":"Theoretical Computer Science"},{"key":"2020040702351779700_ref12","volume-title":"Basic Proof Theory","author":"Troelstra","year":"1996"},{"key":"2020040702351779700_ref13","first-page":"63","article-title":"On intuitionistic modal epistemic logic.","volume":"21,","author":"Williamson","year":"1992","journal-title":"Journal of Philosophical Logic,"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/1\/281\/33016430\/exaa012.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"http:\/\/academic.oup.com\/logcom\/article-pdf\/30\/1\/281\/33016430\/exaa012.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,7]],"date-time":"2020-04-07T06:35:28Z","timestamp":1586241328000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/30\/1\/281\/5739315"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1]]},"references-count":13,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2020,2,20]]},"published-print":{"date-parts":[[2020,1,23]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exaa012","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"value":"0955-792X","type":"print"},{"value":"1465-363X","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2020,1]]},"published":{"date-parts":[[2020,1]]}}}