Fakulta elektrotechnická

České vysoké učení technické v Praze

ČVUT v Praze

Popis předmětu - AE4M33AU

Přehled studia | Přehled oborů | Všechny skupiny předmětů | Všechny předměty | Seznam rolí | Vysvětlivky               Návod
AE4M33AU Automatic Reasoning Rozsah výuky:2+2c
Garanti:Štěpánková O. Role:PO,V Jazyk výuky:EN
Vyučující:Jakubův J., Vyskočil J. Zakončení:Z,ZK
Zodpovědná katedra:13136 Kreditů:6 Semestr:L

Anotace:

Theorem proving is no more restricted to mathematics, but it is ever more often used in situations, when one needs to make sure that the suggested procedure meets the initial requirements it is used in deductive databases as well as for verification of SW or HW components. The process of proof construction has to be automated for that purpose. The course reviews current systems of 1st order theorem proving and their practical applications. There are explained underlying theoretical principles (model checking, resolution, tableaux) together with their practical and theoretical constraints. Special attention is devoted to gaining experience in choosing the best tool to solve a specific problem, in identification of mistakes in input or in strengthening the obtained results.

Výsledek studentské ankety předmětu je zde: AE4M33AU

Osnovy přednášek:

1. History of automated reasoning in the context of artificial intelligence, review of its historical and up-to-date applications.
2. Problems in Boolean domains: from their specification and representation, to the formal solution. Properties of logical theorem proving - correctness and completness.
3. DPLL method, its existing implementations and their practical applications.
4. Model checking as a tool for verification, applications for finite automata.
5. Model checking - existing systems and how they are used in practice.
6. Automated theorem proving in general domains, language of 1st order logic.
7. Resolution and theorem provers based on this paradigma.
8. Workflow in resolution theorem provers and its basic steps: transformation to clausal form, ANL loop.
9. Non-resolution theorem provers: "tableaux", equality, transformation to DPLL.
10. Methods and systems for model construction in general domains.
11. Practical and theoretical boundaries for existing methods and systems.
12. Review of current automated theorem provers, their efficiency and practical utilization.
13. Algorithmic complexity of automated theorem provers and choice of the language for knowledge representation.
14. Spare slot.

Osnovy cvičení:

1. Examples of typical problems for automated reasoning from various domains..
2. Specification of some simple problems in the formal language.
3. Transformation of the specification into the form requested by the theorem prover.
4. The tools for automated theorem proving - hands-on exercise.
5. Specification of more complex problems in the formal language and their automated solution I.
6. Specification of more complex problems in the formal language and their automated solution II.
7. Choice of the tool to be used in a specific problem.
8. Assignment of an individual project its goal is to implement a simple theorem prover applying specific clearly defined strategy or constraint on the used language in order to check impact of this.
9. Transformations of input and output for various theorem provers, interpretation of conclusions.
10. How to find an error in the problem statement.
11. Autonomous work on the assigned project the second part.
12. Simplification and strengthening of the obtained results.
13. Autonomous work on the assigned project the third part.
14. Credits, spare slot.

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
MEKME3 Elektronika V 4
MEKME4 Sítě elektronických komunikací V 4
MEKME5 Komunikační systémy V 4
MEKME2 Multimediální technika V 4
MEKME1 Bezdrátové komunikace V 4
MEOI1 Umělá inteligence PO 4
MEEEM4 Ekonomika a řízení energetiky V 4
MEEEM5 Ekonomika a řízení elektrotechniky V 4
MEEEM1 Technologické systémy V 4
MEEEM2 Elektrické stroje, přístroje a pohony V 4
MEEEM3 Elektroenergetika V 4
MEKYR4 Letecké a kosmické systémy V 4
MEKYR2 Senzory a přístrojová technika V 4
MEKYR3 Systémy a řízení V 4
MEKYR1 Robotika V 4


Stránka vytvořena 23.4.2018 17:47:29, semestry: L/2018-9, Z,L/2017-8, Z/2018-9, 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)
Za obsah odpovídá: doc. Ing. Ivan Jelínek, CSc.