David Stanovský    //

NABÍDKA BAKALÁŘSKÝCH A DIPLOMOVÝCH PRACÍ

BAKALÁŘKY

Automatické dokazování matematických vět
Je dána sada axiomů a domněnka, cílem je najít důkaz této domněnky (pokud existuje). Existuje řada algoritmů a počítačových systémů, které tuto úlohu řeší, viz samostatný kurz (přepokládá se jeho souběžné absolvování). Cílem práce bude implementace nějaké metody. Konkrétní nápady:

• Automatizace metody hintů - jistá pokročilá technika dokazování implementovaná v Prover9, která zatím vyžaduje netriviální lidský vstup; mám jistý nápad, jak věc automatizovat, cílem práce je tento nápad implementovat
• Prezentace rovnicových důkazů - přepis důkazů z Prover9 do klasické formy lemma-důkaz-lemma-důkaz-... s rovnostními důkazy, včetně automatické selekce vhodných lemmat (často používané rovnosti, krátké rovnosti, apod.)
• Automatické zkracování důkazů - automatizace různých technik, které fungují ručně (Kinyonova metoda pomocí hintů, selekce vhodných lemmat, apod.)
• zkrácení/prezentace jednoho konkrétního důkazu z teorie lup, tj. převedení do formy srozumitelné člověku

Automatické hledání modelů
Problém zní, k dané sadě axiomů najít model. Student se seznámí se současnými technikami (redukce na SAT solving, program Paradox) a dále se zaměří na jednu z následujících úloh:

• hledání modelů pomocí CSP solverů
• enumerace modelů až na izomorfismus
• urychlení hledání pomocí přidávání axiomů
• hledání modelů se speciálními vlastnostmi (jednoduché, SI, apod.)

Abelovské a silně abelovské algebry
Téma z univerzální algebry. Cílem je prostudovat různé definice, vlastnosti a příklady (silně) abelovských algeber a vyřešit úlohy z kapitoly 3 knihy Hobby-McKenzie.

Piet (pro učitelství informatiky)
Piet je tzv. esoterický programovací jazyk, jehož kód je formě obrázku, který v lepším případě vypadá jako malba Pieta Mondriaana (v horším je to pouze shluk barevných bodů). Cílem práce je naimplementovat nějaké jednoduché matematické algoritmy s důrazem na výtvarnou stránku. Vhodné pro informatiky se sklonem k umění :-)

DIPLOMKY

Automatické dokazování
Viz výše. Některá z uvedených témat lze rozpracovat na úrovni diplomové práce, případně vymyslíme něco jiného. Předchozí znalost problematiky není nutná.

Automatické hledání modelů
Viz výše. Některá z uvedených témat lze rozpracovat na úrovni diplomové práce, případně vymyslíme něco jiného. Předchozí znalost problematiky není nutná.
Pro diplomku by bylo vhodné např. téma Hledání modelů pomocí polynomiálních rovnic, spočívající převedení problému na řešení soustav polynomiálních rovnic nad konečnými tělesy.

Levodistributivní grupoidy
Pod názvem "quandles" se tyto struktury vyskytují v teorii uzlů, zajímavé jsou však i z čistě algebraického hlediska. Úkolem studenta bude 1) nastudovat literaturu týkající se uzlů a uzlových quandlů, 2) přepracovat přehledový článek zadavatele (který zatím obsahuje jen čistě algebraické výsledky), doplnit jej důkazy a dalšími fakty a dovést do publikovatelné podoby. K dispozici jsou i nějaké otevřené problémy.

Případní zájemci nechť mě kontaktují na výše uvedeném emailu.