Automatické uvažování

Garant předmětu:

Přednášející:

Cvičící:

Předmět zajišťuje:

katedra počítačů

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: http://www.fel.cvut.cz/anketa/aktualni/courses/A4M33AU

Požadavky:

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

Osnova 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

Osnova 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.

Cíle studia:

Studijní materiály:

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

Poznámka:

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

Další informace:

Pro tento předmět se rozvrh nepřipravuje

Předmět je součástí následujících studijních plánů: