Public Syllabus

Academic overview

Programme

AIDC

Period

Year 1, Semester 2

Credits

Weeks

Curriculum placement

Appears in study plans

AIDC (2025 - 2027) Year 1, Semester 2 Elective subject, group 1

Teaching team

Course coordinator

Adrian Crăciun

Seminar coordinators

Adrian Crăciun

Learning time distribution

Total
Curriculum	Lecture	Practice	Total Weekly	Lecture	Practice
42	28	14	3	2	1
Exam hours
4
Individual Study	Bibliography study	Field study	Homework	Tutoring	Others
104	33	14	43	14	0
Overall
150

Learning outcomes

Knowledge

Understand the theoretical foundations of term rewriting, its role as a general framework in computing, its limitations and approaches to overcome these limitations where possible.
Describe terms and operation on terms. Perform operations on terms (substitutions, unification). Define simplification orders for identities, orient identities into rules, compute critical pairs and apply completion procedures. Also, implement the mentioned operations. Describe abstract reduction systems. Understand rewriting as a general framework underlying many formalisms in computer science.
(6a03a0952355ae3a04d2f2ed) Advanced knowledge in the field of logic and automated reasoning;

Skills

Manipulate terms, orient rules, complete rule systems. Implement term operations, termination, completion.
(6a03a0952355ae3a04d2f2fb) conduct research activities in Computer Science and related fields;

Responsibility

Identify situations where term rewriting systems can be employed.
(6a03a0952355ae3a04d2f301) Ethical, honest, and collegial behaviour in professional practice.

Online platform

Google Classroom, access code: tshm6b4.

Course content

Content	Methods	Obs
L1. Motivation. Introductory examples. Abstract rewriting systems (I): Equivalence andreduction.	Q&A/Lecture/Dialogue	2h
L2. Abstract rewriting systems (II):The Church Rosser property. Confluence. Well Founded Induction.	Q&A/Lecture/Dialogue	2h
L3. Abstract rewriting systems (III): Termination orderings. Multiset orderings.	Q&A/Lecture/Dialogue	2h
L4. Terms. Substitutions. Identities.	Q&A/Lecture/Dialogue	2h
L5. Equational problems. Unification of terms.	Q&A/Lecture/Dialogue	2h
L6. Termination. Termination orderings.Simplification orderings. Recursive pathorderings. Knuth-Bendix orderings.	Q&A/Lecture/Dialogue	2h
L7. Confluence. Critical pairs.	Q&A/Lecture/Dialogue	2h
L8. Completion. The basic completion procedure. Implementation issues	Q&A/Lecture/Dialogue	2h
L9. Huet's completion procedure.	Q&A/Lecture/Dialogue	2h
L10. Other CPC algorithms: First order resolution.	Q&A/Lecture/Dialogue	2h
L11. Other CPC algorithms: Groebner Bases (I)	Q&A/Lecture/Dialogue	2h
L12. Other CPC algorithms: Groebner Bases (II)	Q&A/Lecture/Dialogue	2h
L13. Implementation revisited.	Q&A/Lecture/Dialogue	2h
L14. Summary of the lecture, review of material	Q&A/Lecture/Dialogue	2h

Course bibliography

Bibliography:Baader F, Nipkow T. Term Rewriting and All That. Cambridge University Press; 1998.Terese. Term Rewriting Systems. Cambridge University Press, 2003.

Seminar content

Content	Methods	Obs
Lab 1-7. Implementation of concepts introduced in the lectures: terms, term operations, rewriting systems.	Experiment, discussion, team work.	14h
Bibliography:Baader F, Nipkow T. Term Rewriting and All That. Cambridge University Press; 1998.Terese.

Seminar bibliography

The content of the lecture is similar to similar standard lectures in well known and established universities.

Corroboration

(none)

AI tools guidance

Not allowed.

Evaluation and delivery

Activity	Criteria	Methods	Percentage
C	10: excellent (outstanding performance with only minor errors), 8-9: very good (above the average standard but with some errors), 6-7: satisfactory (fair, but with significant shortcomings), 5: sufficient (performance meets minimum criteria), 0-4: fail (significant work has to be done)	Oral exam	70.0%
S	Implementation of a Critical Pair / Completion Algorithm		30.0%

Performance standards

Basic knowledge of the concepts presented in the lecture: explain and apply. Minimal knowledge is measured by reaching the grade for passing the exam (5).