Popis předmětu - AD4M33AU

Přehled studia | Přehled oborů | Všechny skupiny předmětů | Všechny předměty | Seznam rolí | Vysvětlivky               Návod
AD4M33AU Automatické uvažování Rozsah výuky:14KP+6KC
Garanti:  Role:PO,V Jazyk výuky:CS
Vyučující:  Zakončení:Z,ZK
Zodpovědná katedra:13136 Kreditů:6 Semestr:L

Anotace:

Hledání důkazů už není jen součástí matematiky, ale používá se stále častěji i v situacích, kdy je třeba se přesvědčit, že navržený postup nebo řešení splňuje výchozí požadavky setkáváme se s ním nejen v deduktivních databázích, ale i při verifikaci SW nebo HW komponent. Proto je nutné proces tvorby důkazu z daných předpokladů automatizovat. Předmět seznamuje studenty se současnými dokazovacími systémy pro logiku 1.řádu a jejich aplikacemi. Jsou vysvětleny teoretické principy použité při konstrukci systémů automatického dokazování (model checking, rezoluce, tableaux) a jejich praktická i teoretická omezení. Při samostatném řešení konkrétních problémů z oblasti počítačových aplikací student získá zkušenosti, jak vybrat vhodný nástroj pro řešení pro konkrétního problému, jak rozpoznat chybu v zadání či jak zesílit nalezené výsledky.

Výsledek studentské ankety předmětu je zde: A4M33AU

Osnovy přednášek:

1. Historie automatického uvažování v kontextu umělé inteligence, přehled historických a současných aplikaci automatického uvažování.
2. Formulace, reprezentace a řešení úloh v booleovských doménách. Korektnost a úplnost logického odvozování.
3. Metoda DPLL, její existující implementace a praktické použití.
4. Model checking jako nástroj pro verifikaci, aplikace pro konečné automaty.
5. Model checking - existující systémy a jejich praktické použití.
6. Automatické dokazovaní v obecných doménách, formulace a reprezentace problému v predikátové logice.
7. Přehled existujících metod, rezoluční metody.
8. Organizace práce rezolučních dokazovačů: převod do klauzulí, ANL smyčka.
9. Další dokazovací metody: "tableaux", rovnostní dokazování, převod na DPLL.
10. Metody a systémy pro hledání modelu v obecných doménách.
11. Praktické a teoretické limity existujících metod a systémů.
12. Přehled současných dokazovacích systémů, jejich výkonnost a praktické použití.
13. Algoritmická složitost dokazovacích algoritmů a volba použitého jazyka reprezentace.
14. Rezerva

Osnovy cvičení:

1. Příklady typických problémů pro automatické uvažování z různých oblastí.
2. Formalizace zadaných jednoduchých slovních úloh.
3. Převod problému do formalizmu nástrojů pro automatické uvažování.
4. Práce s nástroji pro automatické uvažování.
5. Formalizace dalších slovních problémů a jejich řešení pomocí existujících systémů I.
6. Formalizace dalších slovních problémů a jejich řešení pomocí existujících systémů II.
7. Volba vhodných nástrojů pro řešení pro konkrétního problému.
8. Řešení projektu cílem je na vlastní jednoduché implementaci ověřit, jaký vliv na chování programu automatického dokazování může mít volba použité metody (např. strategie odvozování nebo omezení použitého jazyka).
9. Převody vstupu a výstupu pro různé systémy, interpretace výsledků.
10. Metody hledání chyb v zadáních.
11. Řešení projektu druhá část.
12. Zjednodušování a zesilování nalezených výsledků.
13. Řešení projektu třetí část.
14. Udělování zápočtů, rezerva.

Literatura:

Bundy, A.: The Computational Modelling of Mathematical Reasoning, Academic Press 1983 (Bundy). http://www.inf.ed.ac.uk/teaching/courses/ar/book/book-postcript/ Clarke, E.M. Jr., Grumberg, O. and Peled, D. A.: Model Checking, The MIT Press, 1999, Fourth Printing 2002. http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=3730 McCune, W.: Otter 3.3 Reference Manual (http://www-nix.mcs.anl.gov/AR/otter/otter33.pdf) Newborn, M.: Automated Theorem Proving: Theory and Practice Robinson, J.A., Voronkov, A. (Eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press 2001 Weidenbach, Ch.: SPASS: Combining Superposition, Sorts and Splitting (1999) Wos, L. and Pieper, G.W.: A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning

Požadavky:

Rozpoznávání a strojové učení, Pokročilé metody reprezentace znalosti

Poznámka:

Rozsah výuky v kombinované formě studia: 14p+6c

Předmět je zahrnut do těchto studijních plánů:

Plán Obor Role Dop. semestr
MKOI1 Umělá inteligence PO 4
MKEEM1 Technologické systémy V 4
MKEEM5 Ekonomika a řízení elektrotechniky V 4
MKEEM4 Ekonomika a řízení energetiky V 4
MKEEM3 Elektroenergetika V 4
MKEEM2 Elektrické stroje, přístroje a pohony V 4
MKKME1 Bezdrátové komunikace V 4
MKKME5 Komunikační systémy V 4
MKKME4 Sítě elektronických komunikací V 4
MKKME3 Elektronika V 4
MKKME2 Multimediální technika V 4
MKKYR4 Letecké a kosmické systémy V 4
MKKYR1 Robotika V 4
MKKYR3 Systémy a řízení V 4
MKKYR2 Senzory a přístrojová technika V 4


Stránka vytvořena 21.10.2019 09:50:01, semestry: Z,L/2020-1, L/2018-9, Z,L/2019-20, připomínky k informační náplni zasílejte správci studijních plánů Návrh a realizace: I. Halaška (K336), J. Novák (K336)
Za obsah odpovídá: doc. Ing. Ivan Jelínek, CSc.