Teaching



Introduction to Artificial Intelligence (IAI/ZUM)

Motivaní obrázek

Introductory course on artificial intelligens. The course covers essential concepts necessary for further study of artificial intelligence.

The course covers the following topics among others:

  • search space, uninformed/informed search, heuristic search
  • planning, satisfiability, constraint satisfaction
  • neural networks, evolutionary computing
  • multi-agent systems, games, data mining


The course is provided in Czech and English language and is accompanied by a seminar. Attandants can chose one of several seminars taught in Czech. One seminar is provided in English language.

References:
Peter Norvig, Stuart J. Russell: Artificial intelligence: a modern approach (3rd edition). Prentice Hall/Pearson, 2009.



Last update: 19th Jun 2018



Decision Procedures and Verification

Motivaní obrázek

Výběrová přednáška o logických teoriích a procedurách rozhodující splnitelnost v těchto teoriích s důrazem na aplikaci při verifikaci programů (vyučována na MFF UK).


Na přednášce se bude probírat:

  • rozhodovací procedury pro výrokovou logiku (DPLL, BDD)
  • logické teorie pro rovnost, lineární aritmetiku, bitové vektory, pole a ukazatele
  • kombinování rozhodovacích procedur, SMT
  • ověřování korektnosti programů


Přednáška je doplněna cvičením. V rámci cvičení bude možné mimo klasických úloh na procvičení látky řešit také úlohy implementačního charakteru.


Teaching in English: The lecture will be taught in English if required (study materials in English will be provided).


Přednáška

Topic Slides
1.Propositional Logic, Normal Forms of Formulae, Tseitin Encoding [PDF]
2.SAT Solvers, DPLL, CDCL, 2-watched Literals [PDF]
3BDDs, GSAT, WalkSAT, Warning Propagation [PDF]
4Equality Theory and Uninterpreted Functions [PDF]
5.Decision Procedures for Equality Logic Formulae [PDF]
6.Small Domain Allocation [PDF]
7.Bit Vector Arithmetics [PDF]
8.Decision Procedures for Array and Pointer Logic Formulae [PDF]
9.Combination of Theories, Nelson-Oppen Procedure [PDF]
10.Satisfiability Modulo Theories (SMT) Problem [PDF]
11.Linear Arithmetics [PDF]

Cvičení

TopicTasks
1.Tseitin encoding, NNF properties, modeling[PDF]
2.Problem modeling, encoding of states, simulation of CDCL[PDF]
3.BDDs, MTBDDs, GSAT, WalkSAT, factor graphs[PDF]
4.Equality logic, Ackermann's reduction, circuit equivalence[PDF]
5.Equality graphs, adequate domains[PDF]
6.Small adequate domains[PDF]
7.Bit vectors and bit vector constraints[PDF]
8.Arrays and pointers[PDF]
9.Deciding in combined theories[PDF]
10.Satisfiability Modulo Theories (SMT) Problem[PDF]
11.Linear Arithmetics[PDF]


Automata and Grammars

Motivaní obrázek

Introductory course on theory of formal languages. The course covers essential concepts necessary for further study of computer science (taught at MFF CUNI).

The course covers the following topics among others:

  • formal languages, finite automata, non-determinism, regular expressions
  • enhanced automata - bi-directional, push-down
  • grammars, Chomsky hierarchy
  • Turing machines, algorithmically undecidable problems


The course is provided in Czech and English language and is accompanied by a seminar. Attandants can chose one of several seminars taught in Czech. One seminar is provided in English language.

References:
John E. Hopcroft, Rajeev Motwani, Jeffrey D. Ullman: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 2001.


Přednáška

TémaSlidy
1.Jazyky, konečné automaty, Myhill-Nerodova věta [PDF]
2.Redukce konečných automatů [PDF]
3.Ekvivalence automatů, nedeterminismus [PDF]
4.Uzávěrové vlastnosti a dvousměrný automat [PDF]
5.Regular expressions [PDF]
6.Úvod do Chomského hierarchie [PDF]
7.Regulární a bezkontextové gramatiky [PDF]
8.Bezkontextové gramatiky a zásobníkové automaty [PDF]
9.Zásobníkové automaty [PDF]
10.Vlastnosti bezkontextových jazyků [PDF]
11.Turingovy stroje [PDF]
12.Varianty Turingových strojů [PDF]
13.Rekurzivně spočetné jazyky [PDF]

Lecture

DateTopicSlides
1.Languages, deterministic finite automata, Myhill-Nerode theorem [PDF]
2.Reduction of DFAs [PDF]
3.Equivalence of automata, non-determinism [PDF]
4.Non-determinism and two-way automata [PDF]
5.Regular expressions [PDF]
6.Introduction to Chomsky hierarchy [PDF]
7.Regular and Context-free Grammars [PDF]
8.Context-free grammars and push-down automata [PDF]
9.Push-down automata [PDF]
10.Properties of context-free languages [PDF]
11.Turing machines [PDF]
12.Variants of Turing machines [PDF]

Cvičení

TémaÚlohy
1.Jazyky, konstrukce konečných automatů[PDF]
2.Regulární jazyky, ekvivalence automatů[PDF]
3.Ekvivalence automatů, nedeterminismus[PDF]
4.Nedeterministické automaty a převody[PDF]
5.Regular expressions[PDF]
6.Dvousměrné automaty a jejich převody[PDF]
7.Gramatiky - regulární a bezkontextové[PDF]
8.Více o bezkontextových gramatikách[PDF]
9.Zásobníkové automaty[PDF]
10.Kontextové gramatiky[PDF]
11.Turingovy stroje[PDF]

Seminar

TopicTasks
1.Languages, construction of finite automata[PDF]
2.Regular languages, automata equivalence[PDF]
3.Equivalence of automata, non-determinism[PDF]
4.Non-deterministic automata and reductions[PDF]
5.Regular expressions[PDF]
6.Two-way automata and their reductions[PDF]
7.Grammars - regular and context-free[PDF]
8.More on context-free grammars[PDF]
9.Push-down automata[PDF]
10.Context-sensitive grammars[PDF]
11.Turing machines[PDF]


Student Awards
  • SVOČ 2016 first place for a bachelor thesis by Jakub Střelský under my supervision
    Competing work: Automated Generation of Realistic Terrain Using Machine Learning Techniques
    Award given by: The Union of Czech Mathematicians and Physicists.
     
  • Dean's Award 2014 for a master thesis by Marika Ivanová under my supervision
    Competing work: Adversarial Cooperative Path-Finding
    Award given by: Faculty of Mathematics and Physics, Charles University.
     
  • SVOČ 2014 second place for a master thesis by Marika Ivanová under my supervision
    Competing work: Adversarial Cooperative Path-Finding
    Award given by: The Union of Czech Mathematicians and Physicists.