Constraint systems consist of a set of formulas, a semantic domain and a constraint satisfaction procedure. They are introduced and studied in other lectures. We focus here on constraints on terms, i.e. constraints whose semantic domain is a free term algebra or one of his quotients. Such constraints have attracted a lot of attention recently since they can be nicely combined with other logical formalisms. For instance, they are used in the lecture on constraints and theorem proving; constraints on terms allow to express strategies such as basic or ordered strategies at the formula level (instead of the meta-level) and therefore to be inherited during the deductions. We will sketch briefly many other applications.
Solving equations in term algebras (which is also known as unification) is the most famous constraint solving problem over terms. We spend the first part of the lecture on unification problems. After an introduction to the problematic, we present the general results on unification theory including decidability and unification type of various theories and classes of theories. Then, using a rule-based view of the equation solving process, we show different aspects of the field. Syntactic unification, for which we describe, in an abstract fashion, the classical algorithms of Robinson and Martelli-Montanari. Semantic unification (i.e. equational unification) is then studied. We first look at two examples, giving unification algorithms for commutative and associative-commutative theories. Then we focus on general equational unification.
In a second part, we will describe other constraint systems over terms, whose constraint satisfaction problem is solved by "syntactic techniques", consisting of rewriting the constraint until a solved form is reached. This includes for instance equational formulas (a generalization of unification, allowing arbitrary logical connectives) and ordering constraints on terms, in which the ordering is interpreted as a recursive path ordering. The concepts and methods used in parts 1 and 2 will be illustrated via examples presented in the ELAN langage.
In a third part, we consider constraint solving techniques based on tree automata. Tree automata provide an alternative way of representing the solutions of a contraint on terms, following the idea of the correspondence between automata and logic, a la Büchi. For instance, we consider typing constraints, set constraints, matching and unification problems and encompassment constraints, trying to give both an overview of the results and a uniform presentation.