|
| |
|
|
Dôkazy bezespornosti aritmetiky
Horská, Anna ; Pudlák, Pavel (advisor) ; Hrubeš, Pavel (referee) ; Buss, Samuel (referee)
The thesis consists of two parts. The first one deals with Gentzen's consistency proof of 1935, especially with the impact of his cut elimination strategy on the complexity of the proof. Our analysis of Gentzen's cut elimi- nation strategy, which eliminates uppermost cuts regardless of their comple- xity, yields that, in his proof, Gentzen implicitly applies transfinite induction up to Φω(0) where Φω is the ω-th Veblen function. This is an upper bound and Φω(0) represents an upper bound on heights of cut-free infinitary deriva- tions that Gentzen constructs for sequents derivable in Peano arithmetic (PA). We currently do not know whether this is a lower bound too. The first part also contains a formalization of Gentzen's proof of 1935. Based on the formalization, we see that the transfinite induction mentioned above is the only principle used in the proof that exceeds PA. The second part compares the performance of Gentzen's and Tait's cut elimi- nation strategy in classical propositional logic. Tait's strategy reduces the cut-rank of the derivation. Since the propositional logic does not use inference rules with eigenvariables, we managed to organize the cut elimination in the way that both strategies yield identical cut-free derivations in classical propositional logic.
|
|
| |
|
|
Lower Bounds on Boolean Formula Size
Fojtík, Vít ; Hrubeš, Pavel (advisor) ; Savický, Petr (referee)
The aim of this thesis is to study methods of constructing lower bounds on Boolean formula size. We focus mainly on formal complexity measures, gener- alizing the well-known Krapchenko measure to a class of graph measures, which we thereafter study. We also review one of the other main approaches, using ran- dom restrictions of Boolean functions. This approach has yielded the currently largest lower bounds. Finally, we mention a program for finding super-polynomial bounds based on the KRW conjecture. 1
|
|
| |
|
|
Dôkazy bezespornosti aritmetiky
Horská, Anna ; Pudlák, Pavel (advisor) ; Hrubeš, Pavel (referee) ; Buss, Samuel (referee)
The thesis consists of two parts. The first one deals with Gentzen's consistency proof of 1935, especially with the impact of his cut elimination strategy on the complexity of the proof. Our analysis of Gentzen's cut elimi- nation strategy, which eliminates uppermost cuts regardless of their comple- xity, yields that, in his proof, Gentzen implicitly applies transfinite induction up to Φω(0) where Φω is the ω-th Veblen function. This is an upper bound and Φω(0) represents an upper bound on heights of cut-free infinitary deriva- tions that Gentzen constructs for sequents derivable in Peano arithmetic (PA). We currently do not know whether this is a lower bound too. The first part also contains a formalization of Gentzen's proof of 1935. Based on the formalization, we see that the transfinite induction mentioned above is the only principle used in the proof that exceeds PA. The second part compares the performance of Gentzen's and Tait's cut elimi- nation strategy in classical propositional logic. Tait's strategy reduces the cut-rank of the derivation. Since the propositional logic does not use inference rules with eigenvariables, we managed to organize the cut elimination in the way that both strategies yield identical cut-free derivations in classical propositional logic.
|
|
| |
|
| |
|
| |
|
| |
guest ::
RSS feed.