Joint ESSLLI 2012 course by S. Schmitz and Ph. Schnoebelen.

Will be updated & completed during the course of the week.

- Lecture notes, also available from http://cel.archives-ouvertes.fr/cel-00727025
- Slides for the lecture on August 6th, 2012
- Slides for the lecture on August 7th, 2012
- Slides for the lecture on August 10th, 2012

- Course 2.9.1 at MPRI taught by Ph. Schnoebelen reuses much of this material.
- Here is a general introduction to the algorithmic theory of wqos, presented at ENS Rennes.

Well-quasi-orderings (wqos) are a fundamental tool in logic and computer science. They provide termination arguments in a large number of decidability (or finiteness, regularity, ...) results. In constraint solving, automated deduction, program analysis, and many more fields, wqo's usually appear under the guise of specific tools, like Dickson's Lemma (for tuples of integers), Higman's Lemma (for words and their subwords), Kruskal's Tree Theorem and its variants (for finite trees with embeddings), and recently the Robertson-Seymour Theorem (for graphs and their minors). What is not very well known is that wqo-based proofs have an algorithmic content.

The purpose of this course is to provide an introduction to the complexity-theoretical aspects of wqos, to cover both upper bounds and lower bounds techniques, and provide several applications in logics (e.g. data logics, relevance logic), verification (prominently for well-structured transition systems), and rewriting. Because wqos are in such wide use, we believe this topic to be of relevance to a broad community with interests in complexity theory and decision procedures for logical theories. Our presentation is largely based on recent works that simplify previous results for upper bounds.