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ů. 
  - 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í. 
  - 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