Cut elimination and complexity bounds for intuitionistic epistemic logic

被引：1

作者：

Krupski, Vladimir N. ^{[1
]}

机构：

[1] Lomonosov Moscow State Univ, Fac Mech & Math, Moscow 119991, Russia

来源：

JOURNAL OF LOGIC AND COMPUTATION | 2020年 / 30卷 / 01期

关键词：

Modal logic; intuitionistic epistemic logic; sequent calculus; cut-elimination; PSPACE;

D O I：

10.1093/logcom/exaa012

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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-Heyting-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.

引用

页码：281 / 294

页数：14

共 50 条

[41] From basic logic to quantum logic with cut-elimination
Faggian, C
Sambin, G
[J]. INTERNATIONAL JOURNAL OF THEORETICAL PHYSICS, 1998, 37 (01) : 31 - 37
[42] A CUT ELIMINATION THEOREM FOR STATIONARY-LOGIC
SZABO, ME
[J]. ANNALS OF PURE AND APPLIED LOGIC, 1987, 33 (02) : 181 - 193
[43] Sufficient conditions for cut elimination with complexity analysis
Rasga, Joao
[J]. ANNALS OF PURE AND APPLIED LOGIC, 2007, 149 (1-3) : 81 - 99
[44] Problems of Philosophy. Problem #8: The Epistemic Element in Intuitionistic Logic
[J]. Synthese, 1998, 114 (3) : 497 - 497
[45] Cut-elimination for a logic with definitions and induction
McDowell, R
Miller, D
[J]. THEORETICAL COMPUTER SCIENCE, 2000, 232 (1-2) : 91 - 119
[46] CUT ELIMINATION FOR PROPOSITIONAL DYNAMIC LOGIC WITHOUT
BULL, RA
[J]. ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1992, 38 (02): : 85 - 100
[47] THE MODAL LOGIC OF PROVABILITY, CUT-ELIMINATION
VALENTINI, S
[J]. JOURNAL OF PHILOSOPHICAL LOGIC, 1983, 12 (04) : 471 - 476
[48] Cut elimination and decidability for classical lambek logic
Ilic, Mirjana Isakovic
[J]. JOURNAL OF LOGIC AND COMPUTATION, 2008, 18 (01) : 171 - 199
[49] Cut-Elimination for Quantified Conditional Logic
Benzmuller, Christoph
[J]. JOURNAL OF PHILOSOPHICAL LOGIC, 2017, 46 (03) : 333 - 353
[50] Cut-Elimination for Quantified Conditional Logic
Christoph Benzmüller
[J]. Journal of Philosophical Logic, 2017, 46 : 333 - 353

← 1 2 3 4 5 →