Syntactic Cut-elimination for Common Knowledge | Zendy

Kai Brünnler | Zendy; Thomas Studer | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Syntactic Cut-elimination for Common Knowledge

Author(s) -

Kai Brünnler,

Thomas Studer

Publication year - 2009

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2009.02.038

Subject(s) - sequent , mathematical proof , sequent calculus , inference , mathematics , function (biology) , cut elimination theorem , computer science , calculus (dental) , proof calculus , veblen good , discrete mathematics , rule of inference , upper and lower bounds , algebra over a field , pure mathematics , artificial intelligence , natural deduction , geometry , medicine , mathematical analysis , dentistry , evolutionary biology , biology , neoclassical economics , economics

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 ϕ20 on the depth of proofs, where ϕ is the Veblen function

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research