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 条

[41] Strong normalisation of cut-elimination that simulates β-reduction
Kikuchi, Kentaro
Lengrand, Stephane
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS, 2008, 4962 : 380 - +
[42] CUT-ELIMINATION THEOREM FOR THE LOGIC OF CONSTANT DOMAINS
KASHIMA, R
SHIMURA, T
MATHEMATICAL LOGIC QUARTERLY, 1994, 40 (02) : 153 - 172
[43] Towards an algorithmic construction of cut-elimination procedures
Ciabattoni, Agata
Leitsch, Alexander
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2008, 18 (01) : 81 - 105
[44] Strong normalisation of cut-elimination in classical logic
Urban, C
Bierman, GM
FUNDAMENTA INFORMATICAE, 2001, 45 (1-2) : 123 - 155
[45] COMPLETENESS AND CUT-ELIMINATION IN INTUITIONISTIC TYPE LOGIC
OSSWALD, H
MANUSCRIPTA MATHEMATICA, 1972, 6 (01) : 17 - &
[46] Reducing redundancy in cut-elimination by resolution Preface
Baaz, Matthias
Ciabattoni, Agata
Gabbay, Dov M.
Hetzl, Stefan
Weller, Daniel
JOURNAL OF LOGIC AND COMPUTATION, 2017, 27 (02)
[47] Infinitary Cut-Elimination via Finite Approximations
Acclavio, Matteo
Curzi, Gianluca
Guerrieri, Giulio
32ND EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC, CSL 2024, 2024, 288
[48] Modular cut-elimination: Finding proofs or counterexamples
Ciabattoni, Agata
Terui, Kazushige
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2006, 4246 : 135 - 149
[49] Cut-elimination for Weak Grzegorczyk Logic Go
Rajeev Goré
Revantha Ramanayake
Studia Logica, 2014, 102 : 1 - 27
[50] COMPLETENESS AND CUT-ELIMINATION IN CONSTRUCTIVE INFINITARY ARITHMETICS
SATINDER, PK
NOTICES OF THE AMERICAN MATHEMATICAL SOCIETY, 1971, 18 (07): : 1108 - &

← 1 2 3 4 5 →