|
|
Close Help | ||||||||||||||
9.4.2014 14:00 @ Applied Mathematical Logic
By trying to continue in the sequence (point, line segment, triangle, tetrahedron, ...), we drive at the notion of a higher-dimensional simplex. Put heaps of different simplices together side by side and you get a simplicial complex. Generalising further and allowing ‘gluing’ two faces of a simplex together, we get the notion of a simplicial set. Thus we work with things that are (1) geometric, (2) combinatorial in nature. What is worse: (3) they allow for a categorical treatment. We will look at the interplay of (1),(2),(3) to the extent to which the speaker understands it. Whence the title of the seminar arises.
10.4.2014 14:00 @ Seminář strojového učení
Lukáš Neumann se s námi podělí o něco ze svých výsledků týkajících se detekce a rozpoznávání textu v obrázcích a videu - otevřeného problému počítačového vidění, který má mnoho zajímavých aplikací, počínaje algoritmy pro asistenci nevidomým, přes automatický překlad cizojazyčného textu, až po automatickou indexaci databází na základě jejich textového obsahu (např. Google Street View, Flickr nebo archiv vysílání ČT).
14.4.2014 14:00 @ Ostatní semináře
V přednášce budou ukázány souvislosti Escherovy grafiky "Circle limits IV" s teselací (dlážděním) neeukleidovské hyperbolické roviny rovnoramennými trojúhelníky.
23.4.2014 14:00 @ Applied Mathematical Logic
The notion of a (co)limit lies at the heart of category theory. Unfortunately, limits do not usually commute with colimits. This can be shown somewhat amusingly by inspecting that the equality (a b) + (c d) = (a + c) (b + d) does not always hold for natural numbers. There are, however, some types of limits and colimits that do commute with each other. Finding out for which types of limits and colimits this happens is important not only out of sheer curiosity, but also in applications of category theory. For example, sifted colimits are those colimits that commute with finite products. They play an extremely important role in categorical universal algebra. A characterisation of siftedcolimits is known in the setting of ordinary category theory. When working in enriched category theory, we can characterise preorder-enriched sifted colimits. Our ultimate goal: characterise category-enriched sifted colimits. So far, this is a source of many headaches and not so many results.
30.4.2014 13:30 @ Semináře ISCB ČR
Studie se zabývá srovnáním naměřených hodnot U-238 v moči s odhady těchto hodnot pomocí biokinetických modelů, které jsou založeny na denních inhalačních příjmech U-238 z osobní dozimetrie. Bylo získáno 100 vzorků moči od aktivně pracujících horníků. Pro účely modelu byl obsah U-238 ve vzorku přepočten na denní aktivitu standardizací na očekávané denní množství vyloučeného kreatininu v moči. Denní příjmy byly odvozeny s ohledem na docházku do práce z měsíčních aktivit U-238 zaznamenaných na osobních dozimetrech ALGADE a pohybují se v průměru mezi 0,2 až 8,5 mBq. Vylučovací křivky použité v modelu jsou stanoveny podle programu IMBA pro různé hodnoty parametrů, jako je izotopické složení aerosolu, velikost částic a rozpustnost aerosolu v plicní tekutině. Ukazuje se, že biokinetické modely nadhodnocují. Korelace mezi denní aktivitou U-238 v moči a modelovými hodnotami se pohybuje mezi 0,4 až 0,8 v závislosti na druhu důlní profese a dosahuje podobných hodnot jako korelace mezi denní aktivitou U-238 v moči a příjmy U-238 za poslední měsíc před odběrem či v měsíc odběru. Projekt byl financován Evropskou komisí a Ministerstvem školství, mládeže a tělovýchovy (DOREMI, GA 249689, 7G13001).
30.4.2014 14:00 @ Applied Mathematical Logic
Isabelle/HOL is the most widespread instance of interactive computer proof-assistant Isabelle. It allows to formalize high-order mathematical formulas as well as their proofs in a logical calculus. For this purpose, Isabelle/HOL uses the Isar functional language, which is strongly oriented to human-readability of the resultant code to obtain one of the main advantages of Isabelle - the formal verification understandable to all: to the computer, the user and wide mathematical community. I would like to present you the results of my work on formalization of syntactic part of prof. Hájek’s Basic Fuzzy Logic, respectively the construction of reasoning environment beginning with definitions of connectives of BL, going through the inductive definition of the probability relation, the axiomatization and resulting in proving some theorems in calculus and formalized proof of the local deduction theorem and the others required lemmas.
