Warning
This page is located in archive.

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
courses:a4m33au:osnova [2011/02/09 09:48]
vyskoji1
courses:a4m33au:osnova [2013/10/04 13:02] (current)
Line 9: Line 9:
   - Organizace práce rezolučních dokazovačů:​ převod do klauzulí, ANL smyčka.   - 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ů. ​   - Praktické a teoretické limity existujících metod a systémů. ​
-  - Přehled existujících metod, rezoluční metody. ​+  - 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í. ​   - 3.   ​Metoda DPLL, její existující implementace a praktické použití. ​
   - 4.   Model checking jako nástroj pro verifikaci, aplikace pro konečné automaty.  ​   - 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í. ​   - 5.   Model checking - existující systémy a jejich praktické použití. ​
-  - 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.  ​   - 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í. ​   - 12.   ​Přehled současných dokazovacích systémů, jejich výkonnost a praktické použití. ​
courses/a4m33au/osnova.txt · Last modified: 2013/10/04 13:02 (external edit)