|
|
Proof Complexity of CSP
Gaysin, Azza ; Krajíček, Jan (advisor) ; Kolokolova, Antonina (referee) ; Kompatscher, Michael (referee)
In this thesis we formalize Zhuk's decision algorithm solving in p-time tractable con- straint satisfaction problems (CSPs) in a weak theory of bounded arithmetic W1 1 . As a consequence, we show that tautologies that express the negative instances of such CSPs have polynomial proofs in the quantified propositional calculus G. 1
|
|
|
Spectrum problem
Krejčí, Markéta ; Krajíček, Jan (advisor) ; Kompatscher, Michael (referee)
In this thesis we present the notion of a spectrum of a first-order sentence, including several theorems linking it to computational complexity theory and well-known open problems of Scholz and Asser. We show that there are some interesting subsets of N+ that form a spectrum - either by a direct construction or by applying more advanced theorems. Finally, we prove that spectra are closed under union, intersection, addition and multiplication. 1
|
|
|
Monadic NP sets
Putzer, Martin ; Krajíček, Jan (advisor) ; Honzík, Radek (referee)
Generalised spectra, id est classes finitely axiomatisable in existential second-order logic restricted to finite structures, are known by Fagin's theorem to coincide with members of the complexity class NP. Thereby, the problem of NP being closed under complementation reduces to the problem whether every class of finite struc- tures complementary to a generalised spectrum is, too, a generalised spectrum. Provided P ̸= NP, a proof thereof could then possibly be based on finding a par- ticular generalised spectrum (thereby an NP class) whose complement, while in coNP would not be in NP. Pursuits of such a proof, too, however, have been to no avail. A partial resolution of this problem (itself a special case to so called Asser's problem) is Fagin-Hájek theorem, claiming that a subclass of NP, the class of so called monadic NP sets is not closed under complementation. Reproduc- ing Fagin's original proof of the theorem is the aim of this thesis, along with introducing the reader to all preliminary apparatus needed for the proof. 1
|
|
|
The incompleteness theorems and Berry's paradox
Grego, Maroš ; Krajíček, Jan (advisor) ; Kompatscher, Michael (referee)
This thesis is devoted to a formal presentation of an alternative proof of Gödel's first incompleteness theorem, based on the Berry paradox ("the smallest number not definable in under 57 characters", with this definition having less characters and defining this number). The approach used was suggested by an article by G. Chaitin. We define the Kolmogorov complexity of a natural number m as the binary length of the smallest program for the universal Turing machine that on input 0 outputs the number m. Using a formal argument based on the Berry paradox, we show that the property of a (large enough) number n being a lower bound for the Kolmogorov complexity of a number m is not provable in any consistent recursively axiomatizable extension of Robinson arithmetic. But by a counting argument, for all n, it is true for all but finitely many m. This is used to prove the first incompleteness theorem. Another way (by G. S. Boolos) of formalizing the Berry paradox to prove the same theorem is put in the context of the presented approach. 1
|
|
|
Models of bounded arithmetic
Narusevych, Mykyta ; Krajíček, Jan (advisor) ; Šaroch, Jan (referee)
We study mutual relations of various versions of the pigeonhole principle over bounded arithmetic theory T1 2 (R). The main two variants are the ordinary ontoPHPn+1 n (R), formalizing that R is not the graph of a bijective function from [n + 1] into [n], and its weak version, WPHP2m m (S), formalizing that S is not the graph of an injective function from [2m] into [m]. It is known that: T2 2 (R) proves WPHP2m m (R) (with m universally quantified) and, in fact, also WPHP2m m (S) for all relations S that are □p 1(R) (= polynomial-time definable from R) (J. Paris, A. J. Wilkie and A. R. Woods (1988)), neither I∃1(R) nor T1 2 (R) prove WPHP2m m (R), (J. Paris and A. J. Wilkie (1985) and J. Krajicek (1992)), full T2(R) does not prove ontoPHPn+1 n (R), (M. Ajtai (1988), J. Krajicek, P. Pudlak and A. R. Woods (1991), T. Pitassi, P. Beame and R. Impagliazzo (1993)). We generalize the method of J. Paris and A. J. Wilkie (1985) to show that theory T1 2 (R) plus ∀m WPHP2m m (□p 1(R)) does not prove ontoPHPn+1 n (R). This does follow from results mentioned above but such a combined proof involves complex probabilistic combinatorics which is difficult to modify for other principles. On the other hand our method is more elementary and thus better amenable to other principles. We demonstrate this by proving a...
|
|
|
Pseudofinite structures and limits
Ježil, Ondřej ; Krajíček, Jan (advisor) ; Šaroch, Jan (referee)
For a class of graph instances of a computational problem we define a limit object, relative to some computationally restricted class of functions. The key method here is forcing with random variables where the sample set is taken as instances of some nonstandard size. We study the general theory of these limits, called in the thesis wide limits, and their connection to classical problems such as finding a large clique or with the combinatorial problems associated with the classes of total NP search problems PPA and PPAD. Our main results are several 0-1 laws associated with these limits and existence of a significantly large clique of the wide limit of all graph consisting of one large clique. 1
|
|
|
Region Formation and Transformations of its Roles in Course of the 20th Century: Bohemian-Moravian Highlands
Krajíček, Jan ; Klusáková, Luďa (advisor) ; Janáč, Jiří (referee)
"Region" is nowadays one of the most frequented term in the discourse of the humanities. In the approach of the History, the region is used as a theoretical and methodological concept, whose content has wide range in other social sciences, such as Human Geography and Sociology. This thesis deals with the possibility of the utilization of this term in the historical research applicated on the particular case of the Bohemian- Moravian Highlands. Thesis describes the recent state of the research and the progress in the approach to the term of region. The main concepts which can be used in the case of the Highlands are also shown and described. This particular region was chosen because of its specificity - it's a central periphery, which formed itself into a centralized and institutionalized modern region, the Vysočina Region, during the 20th century. The basic way-out is Anssi Paasi's theory of the shaping of regions. According to it, region can be found in many dimensions in the process of its creation - not just in a physical shape, but also in a symbolic shape, in the making of its identity. Eventually, region has got variable social and economic characteristics. The meaning in which region is percepted and imagined is also changed by these processes of creation - the role of the region is changing...
|
|
|
Analysis of pigments from integument of Graphosoma semipunctatum.
Krajíček, Jan ; Bosáková, Zuzana (advisor) ; Svobodová, Eva (referee)
Pterines belong to an important group of compounds, acting as pigments in many species. Some of them are probably responsible for characteristic coloration of the insect group (Hereroptera). This coloration is considered to be a visual warning signal for optically orientating predators (birds, lizards etc.). In this work, pterines in the species of Graphosoma semipunctatum have been investigated by high performance liquid chromatography. To develope an appropriate separation method, the reverse-phase separation mode with C18 stationary phase (Spherisorb ODS 2) and binary mobile phase (organic modifier/buffer or water) was used. The effect of type and content of organic modifiers (methanol, ethanol, tetrahydrofuran) and concentration of phosphate buffer pH 3.0 (10 - 30 mM) in the mobile phases on retention and separation behavior of the studied pterines (leukopterin, biopterin, xanthopterin, isoxanthopterin and erythropterin) was studied. Under the optimized separation conditions (5/95 (v/v) methanol/20 mM phosphate buffer, pH 3.0, flow rate 0.7 ml.min-1 , UV detection at 290 nm), the extract from the integument of Graphosoma semipunctatum was analyzed.
|
|
|
Silné důkazové systémy
Mikle-Barát, Ondrej ; Krajíček, Jan (advisor) ; Pudlák, Pavel (referee)
R-OBDD is a new Cook-Reckhow propositional proof system based on combination of OBDD proof system and resolution proof system. R-OBDD has the strength of OBDD proof system - hard tautologies for resolution like PHPn or Tseitin contradictions have polynomially sized proofs in R-OBDD (R-OBDD p-simulates OBDD proof system as well as resolution). On the other hand, inference rules of R-OBDD are designed to be similar to inference rules of resolution, thus allowing to create a modified version of DPLL algorithm and possibly using heuristics used in various DPLL-like algorithms. This gives a possibility for a SAT solver more efficient than SAT solvers based on resolution proof system. We present design of a SAT solver, which is an adaptation of DPLL algorithm for the R-OBDD proof system. The algorithm is accompanied with proof of its correctness and we show that the run of the algorithm on an unsatisfiable formula can be transformed into tree-like refutation in the R-OBDD proof system.
|
|
|
Spectrogram generation and their synthesis
Krajíček, Jan ; Bálek, Martin (advisor) ; Pangrác, Ondřej (referee)
The thesis describes generation of time-frequency-intensity graphs (spectrograms) of audio recordings using the Fourier transform. The theoretical possibilities and limitations of spectrogram synthesis (audio reconstruction of a given spectrogram) are discussed and two practical synthesis methods are described, based on reconstruction using pure tones and random noise. Spectrogram generation and both described synthesis methods are implemented in the form of a computer program with a graphical user interface, allowing straightforward configuration of relevant parameters.
|
guest ::
RSS feed.