Automatické uvažování

Přednášející:

Petr Pudlák, Jiří Vyskočil

Cvičící:

Petr Pudlák, Jiří Vyskočil

Předmět zajišťuje:

katedra kybernetiky

Anotace:

Hledání důkazů už není jen součástí matematiky, ale používá se stále častěji i vsituací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 zdaný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ů zoblasti 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 vzadání či jak zesílit nalezené výsledky.

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 vobecný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í zrů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 sná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 vzadá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

Rozvrh na zimní semestr 2011/2012:

Rozvrh není připraven

Rozvrh na letní semestr 2011/2012:

	06:00–08:0008:00–10:0010:00–12:0012:00–14:0014:00–16:0016:00–18:0018:00–20:0020:00–22:0022:00–24:00
Po
Út
St
Čt	místnost KN:E-220 Vyskočil J. Pudlák P. 07:30–09:00 (přednášková par. 1 paralelka 101) Karlovo nám. Laboratoř BIOmístnost KN:E-128 Vyskočil J. Pudlák P. 09:15–10:45 (přednášková par. 1) Karlovo nám. Cvičebna K3místnost KN:E-220 Vyskočil J. Pudlák P. 11:00–12:30 (přednášková par. 1 paralelka 102) Karlovo nám. Laboratoř BIO
Pá

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

• Otevřená informatika - Umělá inteligence (povinný předmět oboru)