Otázka zní: Nalézt efektivní způsob umožňující libovolný výraz daného jazyka přepsat do normální formy ekvivalentní s původním výrazem vzhledem k zadané soustavě identit. Odpovědí je přepisující systém. Základy teorie v rámci teorie grafů.

The question is: To find an efficient way enabling to rewrite an expression in a given language into a normal form, equivalent with the original expression with respect to a given list of identities. The answer is a term rewrite system.

N. Dershowitz, J.-P. Jouannaud: Rewrite systems. Chapter 6, 243--320 in J.~van Leeuwen, ed., Handbook of Theoretical Computer Science, B: Formal Methods and Semantics. North Holland, Amsterdam 1990

A. Zimní semestr:.

1. Základy rovnicové logiky.

2. Konvergence v grafech.

3. Unifikace termů.

4. Kritické dvojice pro přepisující systém.

5. Knuth-Bendixův algoritmus.

B. Letní semestr:.

1. Teorie dobrých kvaziuspořádání.

2. Simplifikační kvaziuspořádání a jeho význam pro termínovanost.

3. Knuth-Bendixovo kvaziuspořádání.

4. Příklad: přepisující systém pro rovnicovou teorii grup.

5. Dershowitzovo kvaziuspořádání.

6. Perfektní baze rovnicových teorií.

A. Winter semester:

1. Foundations of equational logiic.

2. Convergence in graphs.

3. Unification of terms.

4. Critical pairs for term rewrite systems.

5. Knuth-Bendux algorithm.

B. Summer semester:

1. Theory of well quasiorders.

2. Simplification quasiordering and its i,portance for termination.

3. Knuth-Bendix quasiorders.

4. Example: Term rewrite system for the equational theory of groups.

5. Dershowitz quasiorders.

6. Perfect bases of equational theories.