Differences

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

--- courses:a4m33au:osnova [2011/02/09 09:38]
vyskoji1
+++ courses:a4m33au:osnova [2011/02/09 09:45]
vyskoji1
@@ Line 4: / Line 4: @@
 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í.
+  - 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í.
+  - 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í.
-  - 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í:
-  - 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í.
-  - 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í.
@@ Line 35: / Line 34: @@
   - 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
+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