Differences

This shows you the differences between two versions of the page.

--- courses:a4m33au:osnova [2011/02/09 09:45]
vyskoji1
+++ courses:a4m33au:osnova [2013/10/04 13:02]
@@ Line 1: / Line 1: @@
-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:
-  - 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í.
-  - Formulace, reprezentace a řešení úloh v booleovských doménách. Korektnost a úplnost logického odvozování.
-  -  Automatické dokazovaní v obecných doménách, formulace a reprezentace problému v predikátové logice.
-  - Organizace práce rezolučních dokazovačů: převod do klauzulí, ANL smyčka.
-  - Praktické a teoretické limity existujících metod a systémů.
-  - 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í.
-  - 7.   Přehled existujících metod, rezoluční metody.
-  - 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.
-  - 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í:
-  - Příklady jednoduchých slovních úloh pro automatické uvažování.
-  - 1.   Příklady typických problémů pro automatické uvažování z různých oblastí.
-  - 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