Differences

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

--- courses:a4m33au:osnova [2011/02/09 09:44]
vyskoji1
+++ courses:a4m33au:osnova [2013/10/04 13:02] (current)
@@ Line 7: / Line 7: @@
   - 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ů.
+  - Přehled existujících metod, rezoluční metody.
+  - Další dokazovací metody: "tableaux", rovnostní dokazování, převod na DPLL.
   - 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.
-  - 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.