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 条
12345