Seminář o základech informatiky

Tento výzkumný seminář poskytuje prostor pro prezentaci výsledků výzkumu v oblasti návrhu algoritmů, diskrétní matematiky, formálních metod, logiky a souvisejících oblastí teoretické informatiky. Seminář společně organizují výzkumné laboratoře DIMEA, FORMELA a LIVE. Seminář navazuje na seminář FMDSA , který v minulosti pořádala laboratoř FORMELA.

Čas a místo

Seminář se obvykle koná v pondělí ve 14:00 během semestru v místnosti C123 v budově Fakulty informatiky, a to (přibližně) jednou týdně.

Jaro 2026 – přehled harmonogramu

Přednášející

2.2.	Marta Grobelna (TU Mnichov)	Kritéria ukončení pro iteraci hodnot ve souběžných stochastických hrách dosažitelnosti a bezpečnosti
2.3.	Ronen Wdowinski (Technická univerzita v Grazu)	Rekonfigurovatelnost a topologické variace Hallovy věty
9.3.	Stefanie Mohr (Corvolution)	Od univerzity k průmyslu: strojové učení pro detekci spánku a spánkové apnoe
16.3.	Roman Feller (TU Wien)	Rozhodovatelnost interpretovatelnosti
23.3.	Tomáš Nagy (MUNI)	Síla a omezení kanonické redukce pro CSP s nekonečnou doménou
30.3.	František Kardoš (Bordeaux)	Barvení s disjunktními korespondencemi pro grafybez K5-minorů
20.4.	Raju Gupta (SAV Bratislava)	O Vietoris-Ripsových komplexech celočíselných mřížek
27.4.	Jan Dreier (TU Wien)	Matematika a umělá inteligence: Praktický seminář a vize
4.5.	Ashwin Bhaskar (CMI)	Techniky symbolického modelování pro Constraint LTL a jeho rozšíření
11.5.	Johanna Brunar	Pseudosmyčky a barvení nekonečných orientovaných grafů
18.5.	Julien Duron	Komplexnost lineárního sousedství a hustý analog ohraničené expanze
8.6.	Marta Grobelna (TU Mnichov)	Zábava s spojitostí

Nadcházející přednášející

Marta Grobelna: Kritéria zastavení pro iteraci hodnot v souběžných stochastických hrách dosažitelnosti a bezpečnosti

Pondělí 2. února, 14:00, místnost C117

Zabýváme se souběžnými stochastickými hrami (CSG) pro dva hráče s nulovým součtem, které se hrají na grafech s cíli dosažitelnosti a bezpečnosti. Mezi ně patří degenerované třídy, jako jsou Markovovy rozhodovací procesy nebo tahové stochastické hry, které lze řešit lineárním nebo kvadratickým programováním; v praxi však iterace hodnot (VI) předčí ostatní přístupy a je nejčastěji používanou metodou. Podobně i u CSG činí tento praktický výkon z VI atraktivní alternativu ke standardnímu teoretickému řešení pomocí existenční teorie reálných čísel. VI začíná podaproximací hledaných hodnot pro každý stav a iterativně je aktualizuje, přičemž tradičně končí, jakmile jsou dvě po sobě jdoucí aproximace ϵ-blízké. Toto kritérium ukončení však neposkytuje záruky ohledně přesnosti aproximace, což je cílem této práce. Předkládáme ohraničenou (tzv. intervalovou) VI pro CSG: doplňuje standardní VI o konvergující posloupnost nadaproximací a končí, jakmile jsou nadaproximace a podaproximace ϵ-blízké.

Ronen Wdowinski: Rekonfigurovatelnost a topologické variace Hallovy věty

Pondělí 2. března, 14:00, místnost C123

Hallova věta umožňuje odvodit existenci úplného párování v bipartitním grafu, nebo ekvivalentně transversály v systému množin. Pro dokázání existence složitějších kombinatorických objektů vyvinuli Aharoni, Berger, Haxell a Meshulam mocné topologické rozšíření Hallovy věty.

Ukážeme, že tyto topologické metody lze použít k odvození dalších informací o řešeních spojených s příslušnými kombinatorickými objekty, zejména pokud jsou tato řešení spojitá (jako rekonfigurační grafy). Mezi aplikace naší práce patří (často nejlepší možné) dostatečné podmínky pro rekonfigurovatelnost kombinatorických objektů, jako jsou nezávislé transverzalní v grafech, párování v bipartitních hypergrafech a geometrické konfigurace spojené s barevnými větami Hellyho, Carathéodoryho a Tverberga.

Stefanie Mohr: Od univerzity k průmyslu: strojové učení pro detekci spánku a apnoe

Pondělí 9. března, 14:00, místnost C123

V této přednášce popíšu svůj přechod od akademického výzkumu k aplikovanému strojovému učení v malé společnosti zabývající se zdravotnickými technologiemi. Nastíním, jak funguje datová věda v regulovaném produktovém prostředí, kde technická rozhodnutí ovlivňují omezení týkající se spolehlivosti, validace a nasazení. Ústředním příkladem je projekt detekce spánkových fází a apnoe založený na signálech odvozených z EKG a charakteristikách HRV. Představím současné přístupy k modelování, výsledky experimentů a praktické výzvy. Cílem je sdílet poznatky z praxe v průmyslu a podnítit diskusi o metodologických vylepšeních.

Roman Feller: Rozhodovatelnost interpretovatelnosti

Pondělí 16. března, 14:00, místnost C123

Bodirskyho-Pinskerova domněnka tvrdí, že existuje dichotomie P vs. NP-úplná pro výpočetní složitost problémů uspokojování omezení (CSP) redukcí prvního řádu konečně ohraničených homogenních struktur. Je pozoruhodné, že dvě struktury spadající do rozsahu této domněnky mají CSP ekvivalentní z hlediska logaritmického prostoru, jsou-li pp-bi-interpretovatelné, nebo ekvivalentně, jsou-li jejich polymorfní klony topologicky izomorfní. Z posledně jmenovaného vyplývá algebraický přístup, který považuje struktury s topologicky izomorfními klony polymorfismu za ekvivalentní a snaží se identifikovat strukturální důvody obtížnosti či řešitelnosti v topologických klonech.

V tomto příspěvku představím všechny výše zmíněné pojmy a poté ukážu, že ekvivalenční relace pp-bi-interpretovatelnosti, na níž je tento přístup založen, je opodstatněná: Konkrétně ukážu, že je rozhodnutelná za mírných podmínek na šablonách; což vylepšuje výsledky Bodirského, Pinsker a Tsankova ohledně rozhodovatelnosti rovnosti klonů polymorfismu. Na závěr také nastíním, že tento ekvivalenční vztah má z pohledu deskriptivní teorie množin nejnižší možnou složitost, čímž získáme další důkaz o jeho rozumnosti. Jedná se o společnou práci s Michaelem Pinskerem.

Tomáš Nagy: Silné stránky a omezení kanonické redukce pro CSP s nekonečnou doménou

Pondělí 23. března, 14:00, místnost C123

Kanonické polymorfismy hrají klíčovou roli ve všech výsledcích týkajících se dichotomie v oblasti problémů uspokojování omezení (CSP) s nekonečnou doménou. Ve skutečnosti ve většině případů tyto polymorfismy plně zachycují informace o řešitelnosti šablon. Ukážeme, že často zachycují i specifičtější vlastnosti složitosti šablon, jako je jejich řešitelnost metodami lokální konzistence. Na základě těchto zjištění se předpokládalo, že složitost všech CSP s nekonečnou doménou, které lze definovat ve strukturách neschopných simulovat lineární uspořádání (jako jsou grafy či hypergrafy), je zachycena jejich kanonickými polymorfismy. Předkládáme však protipříklad k tomuto tvrzení nad 3-uniformním hypergrafem a diskutujeme, jak lze i nadále použít vhodné zobecnění redukcí používaných v algoritmech s konečnou doménou k charakterizaci řešitelných případů s využitím informací poskytovaných kanonickými polymorfismy. Jedná se o společnou práci s Antoinem Mottetem, Michaelem Pinskerem a Michałem Wronou.

František Kardoš: Barevná schémata s disjunktními korespondencemi pro grafy_{bez K5-minorů}

Pondělí 30. března, 14:00, místnost C117

Thomassen proslul svým důkazem, že každý planární graf je 5-vybratelný. Zkoumáme varianty tohoto výsledku se zaměřením na hledání disjunktních korespondenčních zbarvení v obecnější třídě grafů_{bez K5-minorů}.

Korespondenční zbarvení zobecňují zbarvení podle seznamů následujícím způsobem. Daný graf G a kladné celé číslo t, korespondenční t-pokrytí M přiřazuje každému v ∈ V(G) množinu přípustných barev {_1v, ...,_tv} a každé hraně vw ∈ E(G) přiřazuje párování mezi {_1v, ...,_tv} a {_1w, ...,_tw}. M-barevné zbarvení φ vybírá pro každý vrchol v barvu φ(v) (z množiny {_1v, ...,_tv}) tak, že pro každou hranu vw ∈ E(G) se barvy φ(v), φ(w) navzájem neshodují. Dvě M-barevné barvy _φ1,_φ2 grafu G jsou disjunktní, pokud_φ1 (v) ≠_φ2 (v) pro všechna v ∈ V(G).

Pro každý graf G _{bez K5-minorů} a každou korespondenční 6-pokrývku M grafu G sestrojíme 3 vzájemně disjunktní M-barevné barvení _φ1,_φ2,_φ3. Naopak uvádíme příklady grafů_{bez K5-minorů} a korespondenčních 5-pokrytí M, u nichž nelze najít 3 disjunktní M-barevné barvení.

(společná práce s Wouterem Camesem van Batenburgem a Danielem W. Cranstonem)

Raju Kumar Gupta: O Vietoris-Ripsových komplexech celočíselných mřížek

Pondělí 20. dubna, 14:00, místnost C117

Pro metrický prostor (X, d) a r ≥ 0 je Vietoris–Ripsův komplex VR(X; r) je simplicialní komplex na X, kde konečná množina σ ⊆ X je simplex právě tehdy, když průměr σ je nejvýše r, tj. d(x, y) ≤ r pro všechna x, y ∈ σ.

Uvažujme celočíselnou mřížku ^ℤn jako metrický prostor vybavený _d1-metrikou (standardní metrikou slov v Cayleyově grafu) a označme VR(^ℤn; r) označuje Vietoris–Ripsův komplex ^ℤn podle této metriky. Zaremsky vyslovil domněnku, že VR(^ℤn; r) je smrštitelný pro r ≥ n.

V tomto příspěvku tuto domněnku potvrdíme pro n ≤ 5. Ukážeme, že VR(^ℤ6; r) je smrštitelný pro r ≥ 10. Kromě toho určíme homotopický typ VR(^ℤn; 2) pomocí diskrétní Morseovy teorie a ukážeme, že tyto komplexy jsou homotopicky ekvivalentní klínu spočetně nekonečného počtu kopií 3-sféry ^S3 .

Jan Dreier: Matematika a umělá inteligence: Praktický seminář a vize

Pondělí 27. dubna, 12:00, místnost S211

V uplynulých měsících překročili agenti umělé inteligence, jako jsou Claude Code a OpenAI Codex, prahovou hodnotu schopností, díky čemuž se stali pro mou výzkumnou práci skutečně užitečnými. Zapojuji je do úkolů od vypracovávání důkazů a rešerší literatury až po psaní a korektury článků. V této přednášce představím své nastavení: co funguje, co zatím nefunguje a co by nás mohlo čekat v budoucnu.

Dále se budu zasazovat o formální ověřování matematických článků pomocí agentů umělé inteligence a důkazového systému Lean. Představím předběžné výsledky i vizi, kam by se tento směr mohl ubírat.

Ashwin Bhaskar: Techniky symbolického modelování pro Constraint LTL a jeho rozšíření

Pondělí 4. května, 14:00, místnost C123

Omezená lineární časová logika (CLTL) rozšiřuje LTL na proměnné v nekonečných oblastech, přičemž atomické vzorce vyjadřují omezení hodnot v ohraničených pozicích. Demri a D’Souza ukázali, že splnitelnost CLTL nad celými čísly je PSPACE-úplná, a to pomocí symbolických modelů, které konečně reprezentují nekonečná chování a umožňují uvažování založené na automatech.

V první části přednášky představím CLTL a techniku symbolických modelů, na které tento výsledek spočívá. Ve druhé části ukážu, jak lze stejný přístup přizpůsobit tak, aby (i) bylo možné získat algoritmus v časové složitosti 2EXPTIME pro realizovatelnost v omezeném prostředí se dvěma hráči a (ii) rozšířit CLTL o přístup k neomezené minulosti pomocí regulárních výrazů při zachování rozhodovatelnosti splnitelnosti. Tato část je společnou prací s mým školitelem, M. Praveenem.

Johanna Brunar: Pseudosmyčky a barvení nekonečných orientovaných grafů

Pondělí 11. května, 14:00, místnost C123

V raných fázích systematického výzkumného programu zaměřeného na problémy uspokojování omezení (CSP) patřily mezi první studované problémy ty, které byly indukovány konečnými grafy. Hell a Nešetřil již v roce 1990 ukázali, že každý konečný neorientovaný nebipartitní graf buď vede k NP-úplnému CSP, nebo obsahuje smyčku (v takovém případě je jeho CSP triviální). Tento výsledek byl později rozšířen na konečné orientované grafy. Pokud jde o nekonečno, grafy „nejblíže konečným“ jsou ty, jejichž faktor podle skupiny automorfismů je konečný. Zatímco Hell-Nešetřilova věta pro neorientované grafy byla úspěšně zobecněna do tohoto rámce, orientovaný případ představuje značné výzvy. Poprvé se nám podařilo překonat dosavadní překážky bránící rozšíření výsledků pro orientované grafy z konečné do nekonečné oblasti.

Na základě společné práce s Marcinem Kozikem, Tomášem Nagym, Michaelem Pinskerem a Moritzem Schöbim.

Julien Duron: Lineární složitost sousedství a hustý analog ohraničené expanze

Pondělí 18. května, 14:00, místnost C123

Grafy s ohraničenou degenerací, tj. grafy, u nichž je hustota E/V ohraničena pro všechny podgrafy, představují velmi obecnou a užitečnou třídu řídkých grafů. Nejsou však dostatečně „poslušné“, aby umožnily efektivní algoritmus pro ověřování modelů prvního řádu s pevným parametrem (FPT). Důvodem je, že mohou skrývat libovolně složité struktury v ohraničené vzdálenosti; například 1-poddělení kliky.

Třídy s omezenou expanzí (BE) představují podmnožinu tříd s omezenou degenerací s dodatečnou vlastností, že zůstávají degenerovaně omezené i po kontrakci množin s omezeným poloměrem. Třídy BE jsou zejména „stabilní“ při transdukci prvního řádu v tom smyslu, že jakákoli řídká třída získaná transdukcí z třídy BE je sama o sobě třídou BE.

Třídy BE hrají klíčovou roli v porozumění třídám řídkých grafů a umožňují algoritmy modelové kontroly FO v čase FPT [DKT'10]. Abychom rozšířili naše chápání řídkých tříd do hustého režimu, zajímá nás nalezení vhodného hustého analogu tříd s omezenou expanzí. V této přednášce uvidíme, že lineární komplexnost sousedství, což je velmi kombinatorická vlastnost týkající se rozmanitosti sousedství, charakterizuje tento hustý analog omezené expanze.

Marta Grobelna: Zábava s kontinuitou

Pondělí 8. června, 14:00, místnost C123

V této neformální přednášce o probíhajícím výzkumu se budu zabývat technickým problémem, který vyvstal při studiu konvergenčních argumentů pro iteraci hodnot v souběžných stochastických hrách.

Přirozený doménově-teoretický přístup navrhuje použití Scottovy spojitosti a vět o pevných bodech k prokázání konvergenčních vlastností. Jakmile však do hry vstoupí minimaxové argumenty, požadované předpoklady spojitosti přestávají být tak jednoznačné, což vede k jemné mezeře ve stávajícím důkazu.

Nastíním základní problém, vysvětlím, proč nelze standardní argumenty o spojitosti bezprostředně použít, a představím možný způsob, jak tuto mezeru překlenout. Přednáška je zamýšlena spíše jako technická diskuse o důkazových technikách než jako prezentace hotových výsledků.