Přehled studia |
Přehled oborů |
Všechny skupiny předmětů |
Všechny předměty |
Seznam rolí |
Vysvětlivky
Návod
AD4M33AU |
Automatické uvažování |
Role: | |
Rozsah výuky: | 14KP+6KC |
Katedra: | 13136 |
Jazyk výuky: | CS |
Garanti: | |
Zakončení: | Z,ZK |
Přednášející: | |
Kreditů: | 6 |
Cvičící: | |
Semestr: | L |
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.
Výsledek studentské ankety předmětu je zde:
A4M33AU
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í. |
2. | | Formulace, reprezentace a řešení úloh v booleovských doménách. Korektnost a úplnost logického odvozování. |
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í:
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í. |
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
Poznámka:
Rozsah výuky v kombinované formě studia: 14p+6c |
Předmět je zahrnut do těchto studijních plánů:
Plán |
Obor |
Role |
Dop. semestr |
Stránka vytvořena 22.7.2024 17:51:06, semestry: Z,L/2023-4, Z,L/2024-5, připomínky k informační náplni zasílejte správci studijních plánů |
Návrh a realizace: I. Halaška (K336), J. Novák (K336) |