LTG Logic and Theory Group

• Thursday, 10-12

Lecture room A97
Gebäude der Exakten Wissenschaften ("ExWi" building)
Sidlerstrasse 5

Unification, a central topic in automated reasoning and term rewriting,
involves the search for substitutions that make two
terms "equal". In syntactic unification, the terms should be made identical;
in semantic unification, they should be made equal with respect to some
equational theory (e.g., equal as group or semigroup terms). This latter task
amounts to solving equations in free algebras of the given theory. On the other
hand, solving quasi-equations (implications between sets of equations and
equations) in these free algebras, corresponds to the problem of determining the
admissibility of rules for particular logics or classes of algebras. This seminar
will first cover some of the core ideas and achievements of research into syntactic
and semantic unification, and then explore their relevance for characterizing and
exploiting admissible rules.

Suitable for students interested in logic and in the foundations of mathematics and/or computer science. As justification logics are an active research topic of the TIL group, this seminar is also especially suitable for students interested in current research or considering a thesis in theoretical computer science and logic.

Basic knowledge in mathematical logic and/or theoretical computer science.

The seminar will focus first on the handbook chapter:

F. Baader and W. Snyder. Unification Theory. In J.~A.~Robinson and A.~Voronkov, editors, Handbook of Automated Reasoning volume I, pages 447--533. Elsevier, 2001.
Available for download from: http://www.cs.bu.edu/~snyder/publications/

The following paper will then be considered in some detail:

S. Ghilardi. Unification through Projectivity. Journal of Logic and Computation 7(6), 733--751, 1997.