Přehled studia |
Přehled oborů |
Všechny skupiny předmětů |
Všechny předměty |
Seznam rolí |
Vysvětlivky
Návod
| A4M33AU |
Automatické uvažování |
| Role: | |
Rozsah výuky: | 2P+2C |
| Katedra: | 13136 |
Jazyk výuky: | CS |
| Garanti: | |
Zakončení: | Z,ZK |
| Přednášející: | |
Kreditů: | 6 |
| Cvičící: | |
Semestr: | L |
Webová stránka:
http://cw.felk.cvut.cz/doku.php/courses/a4m33au/start
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 15.9.2024 15:51:01, semestry: Z,L/2024-5, L/2023-4, Z/2025-6, Z/2023-4, 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) |