|
|
History of football club in Kostelec nad Labem
Urban, Josef ; Pokorný, Ladislav (advisor) ; Dlouhý, Martin (referee)
Objektive was to describe the history of the football club Kostelec nad Labem, now TJ Kostelec and the circumstnces under which it originated. Its origins and sport efforts from the beginning to the prezent. I work, besides the introductiion, dividend into two thematic areas: theoretical and practical. The first five chapters focus the theory, the sixth is practical. In the first two chapters set the goals, objectives and hypotheses. The third deals with the characteristis of football. The fourth chapter is devoted to the development of football in the world and in Czech republic. The fifth chapter is the most comprehensive and discusses the origins and history or the football club in that city and its current for mand activities. The six- chapter interview with a football witness, who is also coach youth. This sesction is considered the most important questions are directed and used to verify or reject hypotheses. The work is a compilation charakter and could beneficial both for people who deal with football, but also for those who would like to learn something about the fotmation of football clubs in this country and their beginning.
|
|
|
Systems for formal mathematics
Kunčar, Ondřej ; Urban, Josef (advisor) ; Štěpánek, Petr (referee)
The Mizar type system is a relatively sophisticated system as it allows for many properties, such as independent types, attributes, overloading, subtyping, structures and many others. All these properties make formalization of mathematics more intuitive in Mizar that in other systems. However, there is a need to verify mathematical results formalized in Mizar in other systems, so that belief in consistency of Mizar system is strengthened. Attempts at reconstruction of this type system in other mathematics formalization systems follow directly from this requisite. The present work seeks to reconstruct Mizar type system in HOL Light system. The basic idea here is to represent Mizar types as predicates in this system (HOL Light). The present work also aims at precise description of relevant parts of Mizar type system. The thesis concludes by reviewing some of the insights that were arrived at in the course of designing and implementing suggested reconstruction.
|
|
|
Formalization of the deducibility relation of propositional fuzzy logics
Révay, Petr ; Běhounek, Libor (advisor) ; Urban, Josef (referee)
This bachelor thesis presents the formalization of provability relation of fuzzy logic BL in the environment of a mathematical assistant Isabelle/HOL and also the computer-verified proofs of some theorems and syntactic meta-theorems of this logic. It also provides a description of the process of formalization and describes the tools of Isabelle/HOL used in the code by simple examples. The separate chapter is devoted to the introduction to the logic BL. The formalization has been implemented after studying the documentation and choosing of the appropriate methods of Isabelle/HOL. The formalization allows the software to verify the proofs in the axiomatization of BL, and moreover, of the properties of the provability relation itself. Especially, the proof of the local deduction theorem has been formalized as well as the proofs of the theorems of BL, including the derivations of the redundant axioms BL2 and BL3. The major objective of this bachelor thesis is to explore the possibilities of the proof-checker Isabelle/HOL in terms of fuzzy logic BL. With respect to the obtained results the thesis can be used as the starting point of a wider project of formalization of the others fuzzy logics which are based on the logic BL. Powered by TCPDF (www.tcpdf.org)
|
|
|
Systémy pro formální matematiku
Kunčar, Ondřej ; Urban, Josef (advisor) ; Štěpánek, Petr (referee)
Title: Systems for formal mathematics Author: Ondrěj Kuncˇar Department: Dep. of Theoretical Computer Science and Mathematical Logic Supervisor: Mgr. Josef Urban, Ph.D. Supervisor's e-mail address: josef.urban@gmail.com Abstract: The Mizar type system is a relatively sophisticated system as it allows for many properties, such as independent types, attributes, overloading, subty- ping, structures and many others. All these properties make formalization of mathematics more intuitive in Mizar that in other systems. However, there is a need to verify mathematical results formalized in Mizar in other systems, so that belief in consistency of Mizar system is strengthened. Attempts at recon- struction of this type system in other mathematics formalization systems follow directly from this requisite. The present work seeks to reconstruct Mizar type system in HOL Light system. The basic idea here is to represent Mizar types as predicates in this system (HOL Light). The present work also aims at precise description of relevant parts of Mi- zar type system. The thesis concludes by reviewing some of the insights that were arrived at in the course of designing and implementing suggested reconstruction. Keywords: type system, Mizar, HOL Light 1
|
|
|
Neural modelling of mathematical structures and their extensions
Smolík, Martin ; Urban, Josef (advisor) ; Holub, Štěpán (referee)
In this thesis we aim to build algebraic models in computer using machine learning methods and in particular neural networks. We start with a set of axioms that describe functions, constants and relations and use them to train neural networks approximating them. Every element is represented as a real vector, so that neural networks can operate on them. We also explore and compare different representations. The main focus in this thesis are groups. We train neural representations for cyclic (the simplest) and symmetric (the most complex) groups. Another part of this thesis are experiments with extending such trained models by introducing new "algebraic" elements, not unlike the classic extension of rational numbers Q[ √ 2]. 1
|
|
|
Neural modelling of mathematical structures and their extensions
Smolík, Martin ; Urban, Josef (advisor) ; Holub, Štěpán (referee)
In this thesis we aim to build algebraic models in computer using machine learning methods and in particular neural networks. We start with a set of axioms that describe functions, constants and relations and use them to train neural networks approximating them. Every element is represented as a real vector, so that neural networks can operate on them. We also explore and compare different representations. The main focus in this thesis are groups. We train neural representations for cyclic (the simplest) and symmetric (the most complex) groups. Another part of this thesis are experiments with extending such trained models by introducing new "algebraic" elements, not unlike the classic extension of rational numbers Q[ √ 2]. 1
|
|
|
Mapování historických objektů malých pivovarů v příhraničním regionu
URBAN, Josef
Historical breweries were a very important part the of propeties of the most powerful houses and served as one of the main financial sources. This thesis processes historical facts from the Middle Ages to present, the data is related to individual breweries in villages and cities in the area of Českokrumlovsko. It is focused on basic and general information concerning the year of establishment, basic historical charakteristics, year production and the end of breweries activity. It also presents the point map of the individual breweries divided by the owners and it shows an overview chart with the most significant data.
|
|
|
Formalization of the deducibility relation of propositional fuzzy logics
Révay, Petr ; Běhounek, Libor (advisor) ; Urban, Josef (referee)
This bachelor thesis presents the formalization of provability relation of fuzzy logic BL in the environment of a mathematical assistant Isabelle/HOL and also the computer-verified proofs of some theorems and syntactic meta-theorems of this logic. It also provides a description of the process of formalization and describes the tools of Isabelle/HOL used in the code by simple examples. The separate chapter is devoted to the introduction to the logic BL. The formalization has been implemented after studying the documentation and choosing of the appropriate methods of Isabelle/HOL. The formalization allows the software to verify the proofs in the axiomatization of BL, and moreover, of the properties of the provability relation itself. Especially, the proof of the local deduction theorem has been formalized as well as the proofs of the theorems of BL, including the derivations of the redundant axioms BL2 and BL3. The major objective of this bachelor thesis is to explore the possibilities of the proof-checker Isabelle/HOL in terms of fuzzy logic BL. With respect to the obtained results the thesis can be used as the starting point of a wider project of formalization of the others fuzzy logics which are based on the logic BL. Powered by TCPDF (www.tcpdf.org)
|
|
|
The Luxemburgs and the Apennine Peninsula
Urban, Josef ; Helan, Pavel (advisor) ; Lášek, Jan Blahoslav (referee)
Ve své diplomové práci se jsem se pokusil popsat politickou situaci v Itálii v první třetině 14. století se zaměřením na působení významných osobností Lucemburského rodu v této oblasti. Pro zpracování jsem zvolil léta 1308-1313, 1330-1333 a rok 1337. Zaměřil jsem se hlavně na osobu Jindřicha IV. Lucemburského, jeho nástup k moci, volbu říšským králem a následnou cestu za císařskou korunou. V práci rozebírám reformy, které Jindřich použil při správě Italských měst během cesty na Řím. Dále se zaměřuji na odezvu, kterou jeho působení vyvolávalo u příslušníků dvou hlavních politických směrů v Itálii, tedy u guelfů a ghibelinů, i u francouzského krále Filipa IV. a u papeže Klimenta V. pobývajícího tou dobou v Avignonu. Dále se zaobírám pokusem českého krále Jana Lucemburského a jeho syna Karla o založení Lucemburské signorie na území Lombardie, Toskánska a Emilia Romagna a jejich neúspěšné snahy o udržení tohoto území pod Lucemburskou nadvládou. A Karlovo krátkodobým pokusem o získání území v severní Itálii v roce 1337. Opět se věnuji vlivu jejich působení na politiku měst zmíněných oblastí. Také se okrajově zaměřuji na vliv Jindřicha Lucemburského na spisovatele Danta Alighieriho a jeho dílo "De Monarchia" s Jindřichovo tažením do Říma jako předlohou pro vznik tohoto díla.
|
|
|
History of football club in Kostelec nad Labem
Urban, Josef ; Pokorný, Ladislav (advisor) ; Dlouhý, Martin (referee)
Objektive was to describe the history of the football club Kostelec nad Labem, now TJ Kostelec and the circumstnces under which it originated. Its origins and sport efforts from the beginning to the prezent. I work, besides the introductiion, dividend into two thematic areas: theoretical and practical. The first five chapters focus the theory, the sixth is practical. In the first two chapters set the goals, objectives and hypotheses. The third deals with the characteristis of football. The fourth chapter is devoted to the development of football in the world and in Czech republic. The fifth chapter is the most comprehensive and discusses the origins and history or the football club in that city and its current for mand activities. The six- chapter interview with a football witness, who is also coach youth. This sesction is considered the most important questions are directed and used to verify or reject hypotheses. The work is a compilation charakter and could beneficial both for people who deal with football, but also for those who would like to learn something about the fotmation of football clubs in this country and their beginning.
|
guest ::
RSS feed.