Algorithmic Aspects of WQO Theory - CEL - Cours en ligne Accéder directement au contenu
Cours Année : 2012

Algorithmic Aspects of WQO Theory

Résumé

Well-quasi-orderings (wqos) (Kruskal, 1972) 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 these notes 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. Our presentation is largely based on recent works that simplify previous results for upper bounds (Figueira et al., 2011; Schmitz and Schnoebelen, 2011) and lower bounds (Schnoebelen, 2010a; Haddad et al., 2012), but also contains some original material.
Fichier principal
Vignette du fichier
lecturenotes.pdf (1.09 Mo) Télécharger le fichier
Loading...

Dates et versions

cel-00727025 , version 1 (31-08-2012)
cel-00727025 , version 2 (15-09-2013)

Identifiants

  • HAL Id : cel-00727025 , version 2

Citer

Sylvain Schmitz, Philippe Schnoebelen. Algorithmic Aspects of WQO Theory. Master. France. 2012. ⟨cel-00727025v2⟩
1924 Consultations
1623 Téléchargements

Partager

Gmail Facebook X LinkedIn More