Cut-elimination for provability logics and some results in display logic
A syntactic proof of cut-elimination yields a procedure to eliminate every instance the cut-rule from a derivation in the sequent calculus thus leading to a cut-free derivation. This is a central result in the proof-theory of a logic. In 1983, Valentini  presented a syntactic proof of cut-elimination for the provability logic GL for a traditional Gentzen sequent calculus built from sets, as opposed to multisets, thus avoiding an explicit rule of contraction. From a syntactic point of view...[Show more]
|Collections||Open Access Theses|
|b25699635_Ramanayake_D. R. S..pdf||35.85 MB||Adobe PDF|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.