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.

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. Automatické dokazovaní v obecných doménách, formulace a reprezentace problému v predikátové logice.
4. Organizace práce rezolučních dokazovačů: převod do klauzulí, ANL smyčka.
5. Praktické a teoretické limity existujících metod a systémů.
6. Přehled existujících metod, rezoluční metody.
7. Další dokazovací metody: “tableaux”, rovnostní dokazování, převod na DPLL.
8. 3. Metoda DPLL, její existující implementace a praktické použití.
9. 4. Model checking jako nástroj pro verifikaci, aplikace pro konečné automaty.
10. 5. Model checking - existující systémy a jejich praktické použití.
11. 10. Metody a systémy pro hledání modelu v obecných doménách.
12. 12. Přehled současných dokazovacích systémů, jejich výkonnost a praktické použití.
13. 13. Algoritmická složitost dokazovacích algoritmů a volba použitého jazyka reprezentace.
14. 14. Rezerva

Osnovy cvičení:

1. Příklady jednoduchých slovních úloh pro automatické uvažování.
2. 1. Příklady typických problémů pro automatické uvažování z různých oblastí.
3. 3. Převod problému do formalizmu nástrojů pro automatické uvažování.
4. 4. Práce s nástroji pro automatické uvažování.
5. 5. Formalizace dalších slovních problémů a jejich řešení pomocí existujících systémů I.
6. 6. Formalizace dalších slovních problémů a jejich řešení pomocí existujících systémů II.
7. 7. Volba vhodných nástrojů pro řešení pro konkrétního problému.
8. 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. 9. Převody vstupu a výstupu pro různé systémy, interpretace výsledků.
10. 10. Metody hledání chyb v zadáních.
11. 11. Řešení projektu druhá část.
12. 12. Zjednodušování a zesilování nalezených výsledků.
13. 13. Řešení projektu třetí část.
14. 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