Symbolic Constraint Solving (326.097, 326.0UF)

In this course, we explore the theory and practice of symbolic constraint solving: a foundational tool in computational logic, programming languages, and symbolic artificial intelligence. Students will learn elegant and powerful techniques for solving equations over abstract expressions and identifying patterns within symbolic structures. These techniques have a broad range of applications, from automated reasoning, proof assistants, and term rewriting to declarative programming, type inference, and program analysis, and even in such diverse tasks as query-answering, program repair, software code clone detection, or natural language processing.

The course covers unification, matching, and anti-unification (generalization) across multiple settings: first-order syntactic and equational theories, higher-order expressions, and contexts involving uncertain or vague knowledge, where equality is replaced by quantitative approximation.

Number:	326.097, 326.0UF
Title:	Symbolic Constraint Solving
Lecturer:	Temur Kutsia
Time:	Friday, 12:00-13:30
Place:	S3 047
Language:	English
First meeting:	October 17
Registration:	Via the KUSSS system.

Based on in-class quizzes and presentation.

Please visit the course Moodle page.