CourseWare Wiki
Search
Log In
old
courses
a4m33au
osnova
Warning
This page is located in archive.
Differences
This shows you the differences between two versions of the page.
View differences:
Side by Side
Inline
Go
Link to this comparison view
Go
Go
courses:a4m33au:osnova [2011/02/09 09:50]
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ů.
-
- 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
-
-
courses/a4m33au/osnova.txt
· Last modified: 2013/10/04 13:02 (external edit)