TREE AUTOMATA TECHNIQUES FOR TERM REWRITING

Aart Middeldorp (University of Innsbruck)

Content:

Several decision procedures for properties of term rewrite systems rely on tree automata techniques. In this advanced course basic concepts as well as some applications are discussed. Well-known results on finite automata on strings are extended to (ground) terms. Bottom-up tree automata that define the class of regular tree languages are introduced and closure properties as well as decidability results are presented. The preservation of regular tree languages under term rewriting is studied and it shown how tree automata can represent (binary) relations on ground terms. Moreover, applications of tree automata in term rewriting (termination, confluence, first-order theory, strategies) are presented.

Material:

The course is based on chapter 8 of my course notes, which will be made available to participants.

Background:

Familiarity with term rewriting (from the Baader/Nipkow book or from the basic track of an earlier ISR) is assumed.