Syntactic Cut-elimination for Common Knowledge

被引：1

作者：

Bruennler, Kai ^{[1
]}

Studer, Thomas ^{[1
]}

机构：

[1] Univ Bern, Inst Angew Mathemat & Informat, Bern, Switzerland

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2009年 / 231卷 / 0C期

关键词：

common knowledge; cut elimination; infinitary sequent calculus; deep sequents;

D O I：

10.1016/j.entcs.2009.02.038

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We see a cut-free infinitary sequent system for common knowledge. Its sequents are essentially trees and the inference rules apply deeply inside of these trees. This allows to give a syntactic cut-elimination procedure which yields an upper bound of phi(2)0 on the depth of proofs, where phi is the Veblen function.

引用

页码：227 / 240

页数：14

共 50 条

[31] On the computational complexity of cut-elimination in linear logic
Mairson, HG
Terui, K
THEORETICAL COMPUTER SCIENCE, PROCEEDINGS, 2003, 2841 : 23 - 36
[32] Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents
Gore, Rajeev
Lellmann, Bjoern
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2019, 2019, 11714 : 185 - 202
[33] Quick cut-elimination for strictly positive cuts
Arai, Toshiyasu
ANNALS OF PURE AND APPLIED LOGIC, 2011, 162 (10) : 807 - 815
[34] About cut elimination for logics of common knowledge
Alberucci, L
Jäger, G
ANNALS OF PURE AND APPLIED LOGIC, 2005, 133 (1-3) : 73 - 99
[35] The Cut-Elimination Theorem for Differential Nets with Promotion
Pagani, Michele
TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2009, 5608 : 219 - 233
[36] On Cut-Elimination Arguments for Axiomatic Theories of Truth
Hayashi, Daichi
STUDIA LOGICA, 2022, 110 (03) : 785 - 818
[37] A cut-elimination proof in intuitionistic predicate logic
Borisavljevic, M
ANNALS OF PURE AND APPLIED LOGIC, 1999, 99 (1-3) : 105 - 136
[38] An intensional type theory: Motivation and cut-elimination
Gilmore, PC
JOURNAL OF SYMBOLIC LOGIC, 2001, 66 (01) : 383 - 400
[39] Strong normalisation of cut-elimination in classical logic
Urban, C
Bierman, GM
TYPED LAMBDA CALCULI AND APPLICATIONS, 1999, 1581 : 365 - 380
[40] A note on cut-elimination for classical propositional logic
Pulcini, Gabriele
ARCHIVE FOR MATHEMATICAL LOGIC, 2022, 61 (3-4) : 555 - 565

← 1 2 3 4 5 →