Seminaria ogólnoinstytutowe:

W przygotowywanej pracy doktorskiej zatytułowanej „Metody semantycznej kategoryzacji w zadaniach analizy dokumentów tekstowych” zaproponowano oraz zbadano nowy algorytm semantycznej kategoryzacji dokumentów. Na jego podstawie opracowano nowy algorytm agregacji kategorii, rodzine algorytmów semantycznych klasyfikatorów a takze heterogeniczny komitet klasyfikatorów (łaczacy algorytm semantycznej kategoryzacji i znanych dotad klasyfikatorów). Wramach referatu przedstawie pokrótce ich koncepcje oraz wyniki badan ich skutecznosci.

Algorytm semantycznej kategoryzacji działa bez koniecznosci posiadania specjalnie przygotowanego zbioru uczacego – w jego przypadku wykorzystywane sa juz istniejace zasoby np Wikipedii lub inne dane tego typu, jak np angielskojezyczna struktura taksonomii biomedycznej MeSH. Struktury takie tworzone sa przez ludzi przy okazji innych zastosowan, tak wiec z tego punktu widzenia, nie potrzeba dodatkowo tworzyc specjalnych danych uczacych.

Na potrzeby konstrukcji algorytmu zaadaptowano miary semantycznego podobienstwa, które moga byc uzywane w tego rodzaju zasobach, w szczególnosci słuzyc do opracowanej na ich podstawie metody ujednoznaczniania. Stworzono algorytm do agregacji adaptacyjnej, który pozwala w sposób nienadzorowany rzutowac wyniki kategoryzacji do zbioru kategorii bardziej spójnego z punktu widzenia percepcji uzytkownika. Zaproponowano algorytm klasyfikacji semantycznej bazujacy na metodzie kategoryzacji. Poniewaz opiera sie on na semantyce tekstu, dobrze działa w przypadku tworzenia komitetów, jako dodatek do klasyfikatorów działajacych w oparciu o podejscie typu „worka słów”, szczególnie zas dobrze sprawdza sie w przypadku tekstów z luka semantyczna.

Parametric timed automata are a powerful formalism to reason about, model and verify real-time systems in which some constraints are unknown, or subject to uncertainty. Parameter synthesis using parametric timed automata is very sensitive to the state space explosion problem. To mitigate this problem, we propose two new exploration orders, i.e. the “ranking strategy" and the "priority based strategy", and compare them with existing strategies. We consider both complete parameter synthesis, and counterexample synthesis where the analysis stops as soon as some parameter valuations are found. Besides, the ranking will be adapted in order to first synthesize only our desired parameters. Here, we discuss exploring strategy making parameter synthesizing more efficient. Experimental results using IMITATOR show that our new strategies significantly outperform existing approaches, especially in the counterexample synthesis.

Referat będzie dotyczył Podstaw Matematyki i Informatyki. Jest to powrót do intuicjonizmu Brouwera sprzed przeszło 100 lat. We współczesnej Matematyce, Continuum jest definiowane albo jako zbiór liczb rzeczywistych poprzez ciągi Cauchy'ego albo przekroje Dedekinda, albo jako zupełne liniowo uporządkowane ciało Archimedesowe, albo jako zupełna spójna przestrzeń metryczna. Przedstawiona zostanie ogólna metoda indukcyjnych konstrukcji Continuów prowadzących do ciekawych przestrzeni topologicznych. Z tych konstrukcji wynika nowy dowód Twierdzenia Brouwera (w Analizie intuicjonistycznej), że każda funkcja na przedziale jednostkowym [0; 1] jest ciągła. Pełna praca jest dostępna na https://arxiv.org/abs/1510.02787.

Ciagi binarne o odpowiednich własnosciach statystycznych maja podstawowe zastosowanie w kryptografii i telekomunikacji. Ciagiem de Bruijna rzedu n nazywamy ciag binarny o okresie 2ⁿ, w którym kazdy pod-ciag n-bitowy wystepuje dokładnie jeden raz. Ciagi de Bruijna mozna generowac przy pomocy nieliniowych rejestrów przesuwnych (które sa nieliniowymi rekurencjami). Rekurencje te opisane sa przez funkcje Boolowskie od n-zmiennych [1]. W pracy [2] wykazano twierdzenie, ze majac jeden ciag de Bruijna rzedu n mozna wygenerowac przy pomocy operacji łaczenia skrzyzowanych par stanów wszystkie ciagi de Bruijna rzedu n. W pracy [3] zastosowano operacje łaczenia skrzyzowanych par stanów do konstrukcji ciagów de Bruijna wysokiego rzedu z wykorzystaniem logarytmów Zecha w ciałach skonczonych. Praca [4] podaje przykłady kwadratowych funkcji Boolowskich generujacych ciagi de Bruijna do rzedu n = 29.