- Úvod
- O nás
- Lidé a výzkum
- Knihovna
- Výsledky a ocenění
- Vzdělávání
- Kalendář událostí
Jeden ze současných trendů v teorii důkazů neklasických logik je snaha zapojit více algebraických metod a vyvinout tzv. algebraickou teorii důkazů. Typickým příkladem výsledku směřující tímto směrem je důkaz eliminace řezu stejným způsobem, jakým se v algebře dokazuje uzavřenost na Dedekind-MacNeillovo zúplnění. Další výsledky v tomto směru ukazují, že současná teorie důkazů založená na Gentzenových sekventových kalkulech funguje jen pro logiky se strukturálními axiomy nízké složitosti. Cílem našeho projektu je zobecnit současné metody za účelem rozšíření oblasti, kde lze sekventové kalkuly (v zobecněné podobě) aplikovat. S tím souvisí další cíl projektu, kterým je studium výpočetní složitosti neklasických logik.
01. 01. 2011 - 31. 12. 2015
Centrum excelence - Institut teoretické informatiky (CE-ITI) je výzkumné centrum orientované na teoretickou informatiku a diskétní matematiku. Cílem CE-ITI je být vůdčí a respektovanou výzkumnou institucí v celosvětovém kontextu a hybnou silou české teoretické informatiky a dískrétní matematiky. za tímto účelem je v CE-ITI propojena kapacita nejlepších profesorů, mladých výzkumníků a studentů z vynikajících českých institucí. Klíčové aktivity CE-ITI lze shrnout následovně: 1) Výzkum nejvyšší kvality, speciální pozornost je věnována důležitým otevřeným problémům, aktuálním trendům a novým výzkumným směrům. 2) Výchova nové generace vědců, vyhledávání a podpora talentů. 3) Koordinace a kultivace mezinárodní spolupráce, posilování postavení české informatiky a matematiky v celosvětovém kontextu.
01. 01. 2012 - 31. 12. 2018
Cílem projektu je dále rozvinout metody analytické a kombinatorické teorie čísel používané při studiu distribučních vlastností standardních číselně-teoretických objektů. Pod standardními číselně-teoretickými objekty rozumíme číselné posloupnosti a jejich sytémy, dále množiny aritmetických funkcí, případně aritmetická zobecnění těchto objektů. Mezi charakteristiky distribučních vlastnosti patří globální vlastnosti množiny distribučních funkcí, přítomnost některých specifických vlastností distribučních funkcí udávajících např. typ rovnoměrného rozdělení, a pod. Předmětem studia bude i studium pojmu aritmetické hustoty, vzájemné vztahy mezi jejich různými typy a jejich souvislosti s distribučními vlastnostmi podkladových posloupností, jako i rozvoj metod používaných pro určení jejich hodnot pro konktrétní třídy posloupností. Pozornost bude věnováná i metrickým charakteristikám (Hausdorffova dimenze, Baireova klasifikace apod.) množin číselných posloupností a vlivu vlastností algeber aritmetických funkcí s různými typy konvoluce na aritmetické vlastnosti posloupností jejich hodnot.
01. 01. 2012 - 31. 12. 2015
Epileptický záchvat je charakterizován jako náhlá a náhodná porucha funkce mozku. V předchozí práci in vitro jsme prokázali, že záchvatyjsou předcházeny detekovatelnými změnami v chování neuronů, které korespondují s poklesem dynamické stability neuronálních populací a srůstem pravděpodobnosti vzniku záchvatu. Tento proces přechodu do záchvatu má charakter tzv. kritického chování, které bylo popsáno vdynamice řady komplexních systémů a představuje moderní teorii, která byla úspěšně aplikovaná v klimatologii, či ekologii. V navrhovanémprojektu se zaměříme na studium mechanizmů přechodu do záchvatu a kritického chování v chronickém modelu temporální epilepsie in vivo.Za tímto účelem použijeme integrativní multidisciplinární přístup, který bude kombinovat moderní elektrofyziologické metody s technikamiaktivního testování mozkové dynamiky, metodami počítačového modelování a analýzami z oboru komplexních systémů. Pochopenídynamických principů přechodu do záchvatu by mělo významný dopad na současnou léčbu epilepsie a otevřelo by prostor pro vývojinovativních léčebných postupů.
01. 01. 2014 - 31. 12. 2016
Záměrem tohoto projektu je zkoumat asociativní operace a struktury z geometrického pohledu. Motivací je studium geometrie pláství, což je odvětví diferenciální geometrie. Jak už některé výsledky ukázaly, myšlenky této disciplíny je možné úspěšně přizpůsobit tak, aby charakterizovaly asociativitu úplně uspořádaných monoidů a trojúhelníkových norem názorným a intuitivním způsobem. To dává motivaci pokračovat v tomto výzkumu dále a využít jeho potenciál. cílem projektu je výzkum charakterizace asociativních struktur, především úplně uspořádaných monoidů, které hrají důležitou roli při popisu MTL algeber. Tyto algebry tvoří sémantiky MTL logiky, což je prototypická vícehodnotová logika, která se v současné době těší zájmu velkého množství vědců. Očekávaným výstupem projektu bude nejenom hlubší porozumění nespojitým asociativním operacím, ale i zobecnění geometrie pláství pro obecné případy.
01. 01. 2012 - 31. 12. 2014
Cílem projektu je pokračovat v dlouholeté spolupráci mezi pražským a vídeňským pracovištěm na aplikaci teroie her v oblasti fuzzy logik. Projekt se bude zaměřovate zejména na následující oblasti:a) vzájemný vztah herních sémantik pro fuzzy logiky (dialogické a evaluační hry) a jejich vztah k jiným herním vícehodnotovým sémantikám (pravděpodobnostní sémantika pro logiky podporující nezávislost)b) důsledky herní sémantiky pro studium základních fuzzyx logik (např. problematika tzv. bezpečnostních modelů)c) aplikace kooperativních her v oblasti vícehodnotových logik - formování fuzzy koalic a problém vyjednávání (bargaining)d) aplikace dialogických her pro fuzzy logiky v lingvistice se zaměřením na zobecněné kvanifikátoryVýstupem projektu budpu články publikované v impaktovaných časopisech.
01. 01. 2013 - 31. 12. 2014
Velkou část nákladů vývoje složitých systémů s hlubokou integrací softwaru a fyzikálních komponentů (např. auta, vlaky, letadla) tvoří testování správnosti těchto systémů. Pojem hybridního systému je formalismus pro modelování takových systémů. Výsledky tohoto projektu budou, vůbec poprvé, umožňovat metodám pro formální verifikaci hybridních systémů úspěšně zacházet se systémy velikosti vyskytující se v průmyslu. To se dosáhne integrací metod pro formální verifikaci a automatizovanou falsifikaci/testování. Protože nedávné výsledky v oblasti falsifikace hybridních systémů umí v určitých případech už dnes úspěšně zacházet s obrovskými systémy, a protože v případě softwaru příslušná integrace verifikace a faksifikace měla za výsledek obrovské zlepšení výkonnosti, jsme přesvědčení, že tento přístup bude mít za výsledek příslušný průlom také v oblasti hybridních systémů.
01. 01. 2012 - 31. 12. 2014
Projekt se zabývá iteracními metodami pro rešení nekterých duležitých problému numerické lineární algebry. Projekt zahrnujeanalýzu konvergence, predpodminování, rešení nekorektních úloh, vcetne jejich reálných aplikací. Soustredíme se na studiumkrylovovských metod, konkrétne na otevrené otázky týkající se jejich konvergence a souvisejících maticových aproximacníchproblému, odhady chyb a zastavovací kritéria. Budou studovány ruzné predpodmínovací techniky vcetne nových algoritmuzaložených na neúplných faktorizacích a ortogonalizacních schématech, jakož i blokové predpodmínení pro úlohy sedlovéhobodu. Hodláme analyzovat regularizacní metody pro rešení nekorektních úloh v oblasti zpracování obrazové ci signálovéinformace. Predpokládáme rešení otevrených problému v úlohách úplných nejmenších ctvercu a Golub-Kahanovebidiagonalizaci. Nedílnou soucástí naší práce je široká mezinárodní spolupráce a vybrané reálné aplikace jako je aproximaceamplitudy rozptylu a nukleární magnetická rezonance.
01. 02. 2013 - 31. 01. 2018
01. 04. 2014 - 31. 12. 2016
Navržený projekt bude dále rozvíjet klícové smery výzkumu metod pokoušejících se zmírnit nesoulad mezi presnými asrozumitelnými klasifikátory. Temi jsou extrakce logických pravidel z natrénovaných neuronových sítí a evoluce souboruklasifikacních pravidel pomocí genetických algoritmu, algoritmu mravencích kolonií a podobných optimalizacních algoritmu.Projekt se zameruje na zvýšení presnosti indukce pravidel v dobývání klasifikacních pravidel z dat a na rozpracování novýchmetod pro odvozování srozumitelných pravidel z presných klasifikátoru, jako jsou klasifikátory založené na opernýchvektorech. Bude v této oblasti také provádet teoretický výzkum, konkrétne výzkum vztahu, který vzájemná provázanostpresnosti a srozumitelnosti má k rozdílu mezi deskriptivními a generativními klasifikátory, a bude hledat vhodnou formalizacikonceptu srozumitelnosti klasifikátoru.
01. 02. 2013 - 31. 01. 2016
Smyslem tohoto projektu je pokračování našeho dlouholetého výzkumu a studia krylovovských metod, jež se řadí mezi 10 nejdůležitějších algoritmických myšlenek dvacátého století. Rozsáhlá mezinárodní spolupráce se špičkovými zahraničními institucemi hraje v našem projektu klíčovou roli. Zmiňme je zde alespoň rámcově, přičemž podrobnější popis personálního zastoupení těchto institucí i naší předcházející spolupráce bude následovat níže. Prvním významným partnerem projektu jsou dvě úzce spolupracující pracoviště: Výpočetní laboratoř Oxfordské univerzity (Oxford University Computing Laboratory) a laboratoř Rutherford Appleton Laboratory (RAL), které dohromady tvoří šťastné propojení teoretického a aplikačně zaměřeného výzkumu s ohromným přímým dopadem na vývoj nejmodernějších technologií. Druhým významným partnerem projektu je Technická univerzita v Berlíně, což je v oblasti Scientific Computing, do kterého náš výzkum spadá, opět naprosto špičkové pracoviště (důkazem je např. rozsáhlý a dlouhodobý projekt Matheon http://www.matheon.de/, jehož smyslem je použití a vývoj matematických metod v klíčových technologiích, jež nás obklopují). Konečně třetím velmi významným partnerem je pracoviště CERFACS v Toulouse, konkrétně výzkumný tým Parallel Algorithms. Poznamenejme, že propojení a spolupráce mezi uvedenými pracovišti včetně toho našeho, funguje napříč a vytváří tak významnou síť spolupracujících skupin na poli výpočetní matematiky.
01. 07. 2012 - 30. 06. 2015
Matematická fuzzy logika je symbolická (matematická) logika se stupňovitým pojmem pravdy, kterou je třeba rozlišovat od fuzzy logiky v širokém smyslu, což je vysoce aplikovaná oblast užívající pojem fuzzy množin. Matematická výroková a predikátová logika má přesné pojmy formulí, axiomů a důkazů, sémantiku. Od Hájkovy monografie z roku 1998 se matematická fuzzy logika intenzívně mezinárodně rozvíjela a naše česká skupina hrála v tomto rozvoji velmi důležitou roli. Nynější projekt bude pokračovat v tomto rozvoji a v mezinárodní spolupráci s důrazem jak na čistě teoretické logické studium, tak jeho aplikaci v informatice. Budou zejména vyšetřovány následující oblasti: teorie důkazů a teorie modelů fuzzy logiky, souvislost s jinými logickými systémy, výpočetní a aritmetická složitost, fuzzy logika v sémantickém webu (deskripční logika) a řada dalších logik významných v informatice (epistemická, deontická, dynamická, atd.).
01. 01. 2010 - 31. 12. 2014
Cílem projektu je teoretická analýza vlastností softcomputingových výpočetních modelů vhodných pro zpracování vysoce dimenzionálních složitých dat z hlediska minimalizace modelové složitosti, efektivity učení a schopnosti generalizace. Dále je to využití teoretických výsledků pro návrh hybridních algoritmů metaučení s adaptivní volbou výpočetního modelu a jeho parametrů a implementace těchto algoritmů jako softwarového nástroje v prostředí Java a MATLAB a jejich testování.
21. 03. 2013 - 31. 05. 2016
Vývoj nových funkčních nanomateriálů není možný bez pochopení pravidel a mechanismů operujících při nanoskopických škálách. Naším cílem je přispět k objasnění vzájemné souvislosti magnetismu a atomární struktury v nanostrukturách, zejména v nanostrukturách obsahujících přechodové kovy s nezaplněnými 3d a 4d elektornovými slupkami. Za tím účelem provedeme ab-initio výpočty různých vlastností nanostruktur a budeme sledovat, jak se tyto vlastnosti mění v závislosti na tvaru, velikosti či chemickém složení zkoumaných systémů. Náš přístup se opírá o propojování výpočtů vycházejících z formalismu Greenových funkcí a výpočtů provedených metodou konečných prvků (FEM). Současně s tím budeme dále rozvíjet a vylepšovat metodu konečných prvků a rozšíříme tím možnosti jejího uplatnění v a-initio materiálovém výzkumu. Naše práce tak podnítí další experimentální a technologický výzkum směřující k praktickému využití nanomateriálů, zejména v zařízeních pro uchovávání dat.
01. 01. 2011 - 31. 12. 2015
Formální systémy (ne)klasických logic jsou zasádní pro mnohé oblasti informatiky. Jsou ceneny pro svou deduktivní povahu,universalitu, prenositelnost a možnosti, které plynou z jejich matematických základu. Jednotný prístup založený na teoriiabstraktní algebracké logiky hluboce prispívá ke studiu této široké rodiny logických systému. Cílem projektu je vytvorit variantutéto teorie založenou na pojmu usporádané sémantiky a jejím vztahu k spojce implikace. Usilujeme o vytvorení silnejší, lépeaplikovatelné abstraktní teorie jak pro výrokové tak i pro predikátové logiky. Dále plánujeme demostrovat sílu této teorie nadvou duležitých trídách neklasických logik a to na substrukturálních a fuzzy logikách.
01. 02. 2013 - 31. 01. 2017
NoSCoM je projekt základního výzkumu, který kombinuje několik komplementárních podoborů teoretické informatiky se záměrem prohloubit naše znalosti důležitých specializovaných nestandardních výpočetních modelů. Jeho cílem je charakterizovat výpočetní sílu a efektivitu těchto modelů a prozkoumat jejich schopnost modelovat problémy z vybraných aplikačních domén jako jsou teorie složitosti, lingvistika a strojové učení. Náš vícemodelový přístup bude také zahrnovat analýzu nových zdrojů nebo měr efektivních výpočtů, které jsou zavedeny v příslušných nestandardních výpočetních modelech. Výzkum bude konkrétně zaměřen na neuniformní amorfní výpočetní systémy, které modelují mobilní senzorické sítě, nanostroje, formální modely praktických neurovýpočtů v ÚI, specializované neomezené automaty a gramatiky s důležitými aplikacemi v lingvistice (např. míry volnosti slovosledu), větvící programy pro studium prostorově-složitostních aspektů výpočtů, modely pro aproximaci distribucí empirických dat jako jsou náhodné lesy.
01. 01. 2010 - 31. 12. 2014
Soucasná psychologická teorie nabízí komplexní popis psychických funkcí a osobnosti. Obecne je prijímaná existence vazbypsychických funkcí na mozek jako jejich substrát a z toho vyplývající souvislost osobnosti s mozkovou strukturou a funkcí.Detaily tohoto vztahu však nejsou zrejmé.Rychle se rozvíjející oblastí výzkumu mozku je studium spontánní mozkové aktivity s pomocí funkcní magnetické rezonance,umožnující soucasnou charakterizaci rady mozkových sítí.Tento projekt bude zkoumat vazbu “mind-brain” s využitím merení endogenních vzorcu mozkové aktivity.Zameríme se rovnež na zefektivnení výzkumu této vazby merením aktivity mozku behem stavu “prirozeného sledování” bohatékvazi-realistické audiovizuální stimulace.Kombinovaná psychometrická a neurozobrazovací studie umožní popis souvislostí specifických rysu funkcních mozkových sítí aosobnosti. Výsledky budou dány do kontextu skrze studium vztahu k anatomické strukture mozku, prostrednictvím analýzy data teoretických modelu.
01. 02. 2013 - 31. 01. 2016
Pro úspech krátkodobé predpovedi pocasí je podstatná efektivní asimilace dat dostupných v okamžiku predpovedi, napr.radarových a satelitních dat, do numerického predpovedního modelu pocasí. Cílem projektu je zavedení kvalitativne novýchasimilacních metod.V projektu budou vyvíjeny asimilacní metody využívající techniky pocházející z teorie rozpoznávání obrazcu (zejm.automatickou registraci a morphing). Tyto metody korigují polohy objektu, jako napr. srážkových oblastí, a soucasne korigují ihodnoty fyzikálních promenných. Metody budou zobecnovány tak, aby mohly být použity pro asimilaci radarových a dalšíchmeteorologických dat. Predpokládáme, že tento postup korekce umístení meteorologických útvaru v prostoru i v case povede kezpresnení predpovedi.V projektu budou dále vyvíjeny metody založené na teorii náhodných polí využívající waveletove transformace. Nárocnématicové výpocty v ensemblovém Kalmanove filtru budou nahrazeny efektivními algoritmy waveletové transformace. Metodytaké umožní podstatnou redukci poctu clenu ensemblu.
01. 02. 2013 - 31. 01. 2017
Hlavním cílem je návrh pokročilých predikčních metod pro krátkodobou předpověď výroby elektrické energie z fotovoltaických zdrojů. Tohoto cíle bude dosaženo na základě kombinací znalostí řešitelského týmu z oblasti statistického a obecně nelineárního modelování komplexních systémů a zároveň z oblasti numerického modelování a předpovědi počasí.
01. 03. 2012 - 31. 12. 2014
Vícehodnotový přístup nabízí efektivní nástroje pro tvorbu modelů v teorii her a analýzu ekonomických optim i ekvilibrií. Cílem tohoto projektu je využití metod mnohoznačné analýzy a vícehodnotové logiky k zevrubnému výzkumu několika vybraných náročných problémů teorie her. Náš přístup zahrnuje kooperativní i nekooperativní modely. Budeme analyzovat stabilitu a citlivost ekonomických úloh vedoucích na zobecněné Nashovo ekvilibrium a optimalizovat pobídkovou strategii pro spotový trh Evropské energetické burzy. Zvláštní pozornost bude věnována kooperativním hrám s fuzzy koalicemi a návrhu dynamických vyjednávacích procedur pro jejich jádro. Aplikace vícehodnotové a dynamické epistemické logiky nám umožní nejen zachytit tok informace a znalostí ve hrách, ale postihnout i nejistotu v datech úlohy. Vícehodnotovost prostupuje všechny uvedené herní modely jak na straně popisu hry, tak i jejího řešení.
01. 01. 2012 - 31. 12. 2014
Cílem projektu je vytěžit maximum informací z dat získaných na experimentu D0 během provozu detektoru částic, který zaznamenává události po srážkách protonů a antiprotonů na urychlovači Tevatron. Experiment D0 je součástí prestižnílaboratoře Fermilab v USA zabývající se převážně fyzikou částic s vysokými energiemi a ní souvisejícím základnímvýzkumem. Záměrem předkládaného projektu je použít při zpracovaní dat pokročilé statisticky orientované robustnímetody separace (Fuzzy klasifikace s řízeným dohledem, Support Vector Machines, Model-Based klasifikace, Divergenční metody, apod.) i nestatistické postupy jako jsou geneticky optimalizované neuronové sítě a fraktální analýza. Výsledkem budou nové ověřené metodiky hledání a potvrzování existence nových částic s použitím vyvinutých metod, zpřesnění fyzikálních vlastností těchto částic a upřesnění charakteristik zkoumaných rozpadových procesů. Očekáváme, že nově vytvořené separační a klasifikační metody budou použitelné i v jiných oblastech vytěžování dat včetně budoucích dat na LHC v CERN. Nově navržené a odzkoušené metody budou vyvíjeny v návaznosti na standardně používané postupy částicové fyziky COLLIE, MVA, BDT, SVD, Bayes, apod. a s těmito standardními metodami budou srovnány vzhledem k přesnosti detekce rozpadových částic, robustnosti a eficience metod.
01. 03. 2012 - 31. 12. 2014
Předmětem projektu je návrh řešení problematiky nedostatku parkovacích míst pro těžkou nákladní dopravu, především na dálniční síti, jež plyne z dlouhodobého trendu nárůstu objemu dopravy. Na základě analýzy situace a řady výzkumných projektů okolních států Evropy si projekt kladě za cíl navrhnout systém, který bude na základě vstupních dat z mýtného systému modelovat predikci obsazenosti jednotlivých parkovacích míst tak, aby optimalizoval jejich využití.
01. 01. 2012 - 31. 12. 2014