Popis předmětu - A4M33AU

Přehled studia | Přehled oborů | Všechny skupiny předmětů | Všechny předměty | Seznam rolí | Vysvětlivky               Návod
A4M33AU Automatické uvažování Rozsah výuky:2P+2C
Garanti:Štěpánková O. Role:PO,V Jazyk výuky:CS
Vyučující:Jakubův J., Vyskočil J. 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

Webová stránka:

http://cw.felk.cvut.cz/doku.php/courses/a4m33au/start

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

Plán Obor Role Dop. semestr
MPIB Před zařazením do oboru V
MPKME1 Bezdrátové komunikace V 4
MPKME5 Komunikační systémy V 4
MPKME4 Sítě elektronických komunikací V 4
MPKME3 Elektronika V 4
MPKME2 Multimediální technika V 4
MPOI1 Umělá inteligence PO 4
MPEEM1 Technologické systémy V 4
MPEEM5 Ekonomika a řízení elektrotechniky V 4
MPEEM4 Ekonomika a řízení energetiky V 4
MPEEM3 Elektroenergetika V 4
MPEEM2 Elektrické stroje, přístroje a pohony V 4
MPKYR4 Letecké a kosmické systémy V 4
MPKYR1 Robotika V 4
MPKYR3 Systémy a řízení V 4
MPKYR2 Senzory a přístrojová technika V 4


Stránka vytvořena 18.9.2019 17:51:33, 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.