- Propositional logic, Boolean algebra, propositional resolution, SAT-2KNF
- Predicate logic, unification, predicate logic resolution
- Temporal Logics (LTL, CTL)
- Deterministic finite automata, definition and construction
- Regular languages, closure properties, word problem, string matching

- Nondeterministic automata: 
Rabin-Scott transformation of nondeterministic into deterministic automata
- Epsilon automata, minimization of automata,
elimination of e-edges, uniqueness of the minimal automaton (modulo renaming of states)
- Myhill-Nerode Theorem: 
Correctness of the minimization procedure, equivalence classes of strings induced by automata

- Pumping Lemma for regular languages:
provision of a tool which, in some cases, can be used to show that a finite automaton principally cannot be expressive enough to solve a word problem for some given language

- Regular expressions vs. finite automata:
Equivalence of formalisms, systematic transformation of representations, reductions

- Pushdown automata and context-free grammars:
Definition of pushdown automata, definition of context-free grammars, derivations, parse trees, ambiguities, pumping lemma for context-free grammars, transformation of formalisms (from pushdown automata to context-free grammars and back)
- Chomsky normal form
- CYK algorithm for deciding the word problem for context-free grammrs
- Deterministic pushdown automata

- Deterministic vs. nondeterministic pushdown automata:
Application for parsing, LL(k) or LR(k) grammars and parsers vs. deterministic pushdown automata, compiler compiler
- Regular grammars
- Outlook: Turing machines and linear bounded automata vs general and context-sensitive grammars
- Chomsky hierarchy

- Mealy- and Moore automata:
Automata with output (w/o accepting states), infinite state sequences, automata networks
- Omega automata: Automata for infinite input words, Büchi automata, representation of state transition systems, verification w.r.t. temporal logic specifications (in particular LTL)

- LTL safety conditions and model checking with Büchi automata, relationships between automata and logic
- Fixed points, propositional mu-calculus

- Characterization of regular languages by monadic second-order logic (MSO)

- Logik für Informatiker Uwe Schöning, Spektrum, 5. Aufl.

- Logik für Informatiker Martin Kreuzer, Stefan Kühling, Pearson Studium, 2006
- Grundkurs Theoretische Informatik, Gottfried Vossen, Kurt-Ulrich Witt, Vieweg-Verlag, 2010.
- Principles of Model Checking, Christel Baier, Joost-Pieter Katoen, The MIT Press, 2007