Term Rewriting Systems - NALG011

• Title: Přepisující systémy
• Guaranteed by: Department of Algebra (32-KA)
• Faculty: Faculty of Mathematics and Physics
• Actual: from 2011 to 2017
• Semester: winter
• E-Credits: 6
• Hours per week, examination: winter s.:2/0, --- [HT]; summer s.:2/0, Ex [HT]
• Capacity: unlimited
• Min. number of students: unlimited
• 4EU+: no
• Virtual mobility / capacity: no
• State of the course: not taught
• Language: Czech
• Teaching methods: full-time
• Teaching methods: full-time
• Classification: Informatics > Theoretical Computer Science; Mathematics > Algebra
• Co-requisite : NALG103

Annotation

English

Last update: T_KA (25.05.2001)

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.

Czech

Last update: ()

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ů.

Literature

Last update: RNDr. Pavel Zakouřil, Ph.D. (05.08.2002)

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

Syllabus

English

Last update: T_KA (26.04.2004)

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.

Czech

Last update: ()

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í.