- Ú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
Umělá inteligence v mnoha svých podoblastech dosáhla dospělosti a jejím aktuálním trendem je integrování vytvořených technik pro řešení těžkých reálných problémů jako je návrh auta bez řidiče nebo vesmírných či podvodních průzkumných robotů a dronů. Projekt se zabývánávrhem autonomních agentů (robotů), kteří umí vytvářet a upravovat svůj vnitřní model a dělat vlastní rozhodnutí. Zaměřen je na vnitřní znalostní model autonomních agentů, který je vhodný pro plánování jejich chování a který lze získat a upravovat (polo-)automaticky bez nutnosti jeho ručního kódování. Model bude hlavní částí modulární architektury a bude navržen integrací výsledků z oblastí robotiky, plánování, zpracování neurčitosti, reprezentace znalostí, přírodou inspirovaného počítání a lingvistiky. Kromě teoretických výsledků (modely a algoritmy) bude důležitým výstupem také ověření vytvořených technik na reálných robotech. Účelem projektu je přiblížit různé výzkumnéoblasti a uvést jejich výsledky do praxe.
01. 01. 2015 - 31. 12. 2017
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
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íčové směry výzkumu metod pokoušejících se zmírnit nesoulad mezi přesnými a srozumitelnými klasifikátory. Těmi jsou extrakce logických pravidel z natrénovaných neuronových sítí a evoluce souborů klasifikačních pravidel pomocí genetických algoritmů, algoritmů mravenčích kolonií a podobných optimalizačních algoritmů. Projekt se zaměřuje na zvýšení přesnosti indukce pravidel v dobývání klasifikačních pravidel z dat a na rozpracování nových metod pro odvozování srozumitelných pravidel z přesných klasifikátorů, jako jsou klasifikátory založené na opěrných vektorech. Bude v této oblasti také provádět teoretický výzkum, konkrétně výzkum vztahu, který vzájemná provázanost přesnosti a srozumitelnosti má k rozdílu mezi deskriptivními a generativními klasifikátory, a bude hledat vhodnou formalizaci konceptů srozumitelnosti klasifikátorů.
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
Projekt přispěje k budování teoretických základů neuropočítání. Cílem výzkumu je získat nové znalosti ve formě matematických výsledků popisujících schopnosti a omezení vícevrstvých sítí. Budou popsány vztahy mezi sítěmi s různými typy jednotek (perceptrony, radiálními a jádrovými) a různými parametry těchto jednotek. Budou odvozeny odhady modelové složitosti sítí v závislosti na vstupních dimenzích,počtech a typech jednotek a architekturách sítí. Budou charakterizovány vlastnosti vysoce dimenzionálních úloh, které lze reprezentovat nebo aproximovat sítěmi s přijatelnou složitostí. Budou analyzována optimální řešení úloh učení z hlediska generalizace a modelové složitosti.
01. 01. 2015 - 31. 12. 2017
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ágní kvantifikátory (např. "málo", "mnoho" či "zhruba polovina") představují závažný problém při automatickém zpracování přirozeného jazyka. Navržení uspokojivé teorie vágních kvantifikátorů vyžaduje vytvoření formálních modelů a posouzení jejich adekvátnosti z hlediska lingvistiky, strojového odvozování a začlenitelnosti do širších logických systémů; tento výzkumný úkol zahrnuje náročné problémy v oblasti informatiky, logiky, lingvistiky i analytické filosofie. Fuzzy logika, založená na pojmu stupňů pravdivosti, poskytuje matematické metody pro modelování některých aspektů vágnosti; její využívání pro práci s vágními kvantifikátory však doposud z velké části opomíjelo možnosti deduktivních systémů studovaných v rámci matematické fuzzy logiky. Cílem projektu je prohloubit a rozšířit matematické základy modelování vágních kvantifikátorů pomocí aparátu a metod matematické fuzzy logiky, včetně dvojúrovňové modální logiky, herní sémantiky a metod strojového usuzování.
01. 01. 2015 - 31. 12. 2017
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 logik jsou zásadní pro mnohé oblasti informatiky. Jsou ceněny pro svou deduktivní povahu, universalitu, přenositelnost a možnosti, které plynou z jejich matematických základů. Jednotný přístup založený na teorii abstraktní algebraické logiky hluboce přispívá ke studiu této široké rodiny logických systémů. Cílem projektu je vytvořit variantu této teorie založenou na pojmu uspořádané sémantiky a jejím vztahu k spojce implikace. Usilujeme o vytvoření silnější, lépe aplikovatelné abstraktní teorie jak pro výrokové tak i pro predikátové logiky. Dále plánujeme demonstrovat sílu této teorie na dvou důležitých třídách neklasických logik a to na substrukturálních a fuzzy logikách.
01. 02. 2013 - 31. 01. 2017
Podstatou projektu je popsat současný stav přijímacích řízení na české vysoké školy a připravit metodologii pro vývoj standardizovaných přijímacích testů. Projekt pokrývá celý cyklus vývoje testů – od stanovení cílů, návrhu testu, psaní, oponování a pretestování položek, až po zadání testu a jeho následnou validizaci. Zvláštní pozornost je věnována moderním psychometrickým nástrojům potřebným ke skórování studentů, kalibraci položek, detekci nevhodných položek, odhadu reliability a validity testu v komplexních designech, jakož i skórování a volbě položky v automatizovaných adaptivních estech. Teoretické poznatky jsou implementovány a demonstrovány na reálných datech z přijímacího řízení na lékařskou fakultu.
01. 01. 2015 - 31. 12. 2017
Současná psychologická teorie nabízí komplexní popis psychických funkcí a osobností. Obecně je přijímaná existence vazby psychický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 zřejmé. Rychle se rozvíjející oblastí výzkumu mozku je studium spontánní mozkové aktivity s pomocí funkční magnetické rezonance, umožňující současnou charakterizaci řady mozkových sítí. Tento projekt bude zkoumat vazbu “mind-brain” s využitím měření endogenních vzorců mozkové aktivity. Zaměříme se rovněž na zefektivnění výzkumu této vazby měřením aktivity mozku během stavu “přirozeného sledování” bohaté kvazi-realistické audiovizuální stimulace. Kombinovaná psychometrická a neurozobrazovací studie umožní popis souvislostí specifických rysů funkčních mozkových sítí a osobností. Výsledky budou dány do kontextu skrze studium vztahů k anatomické struktuře mozku, prostřednictvím analýzy dat a teoretických modelů.
01. 02. 2013 - 31. 01. 2016
Pro úspěch krátkodobé předpovědi počasí je podstatná efektivní asimilace dat dostupných v okamžiku předpovědi, např. radarových a satelitních dat, do numerického předpovědního modelu počasí. Cílem projektu je zavedení kvalitativně nových asimilačních metod. V projektu budou vyvíjeny asimilační metody využívající techniky pocházející z teorie rozpoznávání obrazců (zejm. automatickou registraci a morphing). Tyto metody korigují polohy objektu, jako např. srážkových oblastí, a současně korigují i hodnoty fyzikálních proměnných. Metody budou zobecňovány tak, aby mohly být použity pro asimilaci radarových a dalších meteorologických dat. Předpokládáme, že tento postup korekce umístění meteorologických útvarů v prostoru i v čase povede ke zpřesnění předpovědi. V projektu budou dále vyvíjeny metody založené na teorii náhodných polí využívající waveletové transformace. Náročné maticové výpočty v ensemblovém Kalmanově filtru budou nahrazeny efektivními algoritmy waveletové transformace. Metody také umožní podstatnou redukci počtu členů ensemblu.
01. 02. 2013 - 31. 01. 2017
Tématem projektu je výzkum svazově uspořádaných monoidů se zvláštním důrazem na ty, které jsou úplně uspořádané. Protože dosud známé metody pro zkoumání této oblasti matematiky se zdají být vyčerpané, je záměrem projektu využít nových metod, jejichž podstata je geometrická, pro řešení těchto algebraických otázek novým způsobem. Mezi tyto nové nástroje patří geometrie tkání, což je odvětví diferenciální geometrie zavedené Blashkem a Bolem, a reprezentace pomocí Cayleyho monoidů; oba tyto přístupy dovolují přehledným způsobem geometricky zobrazit algebraické vlastnosti struktur.
01. 01. 2015 - 31. 12. 2017
Jedním z nejdůležitějších nástrojů v oblasti formální verifikace jsou invarianty. Invariantem nazýváme množinu stavů daného systému, pro kterou platí, že každý dosažitelný stav systému náleží do této množiny. V poslední době došlo k velkému vývoji metod pro výpočet invariantů založených na dodržení omezujících podmínek, kdy výpočet invariantu je redukován na řešení problému s omezeními v rozhodnutelné teorii. Nicméně, takový postup nelze použít v případech, ve kterých je patřičná teorie nerozhodnutelná a nebo dostupné nástroje nejsou dost efektivní pro v praxi zajímavé úlohy. Tento návrh se zabývá výpočtem invariantů pro hybridní dynamické systémy, což jsou systémy, které mají částečné diskrétní a částečně spojité chování. Proto, abychom se vyhnuli již zmíněným problémům s nerozhodnutelností anedostatečnou efektivností dostupných nástrojů, zvolíme značně odlišný způsob, který využívá robustnosti a simulací.
01. 01. 2015 - 31. 12. 2017