ISR 2010

5th International School on Rewriting

3 – 8 July 2010, Drift 21, Utrecht, Netherlands

Tree Automata and Rewriting

Lecturer

Ralf Treinen (PPS, Université Paris Diderot, France)

Introduction

(advanced track, 3 lecture sessions)

use (word-) automata to solve decision problems of FO theories (Büchi's encoding of Presburger arithmetic, works of Blumensath and Grädel)

tree automata: basic properties, extensions to constrained automata (taking stuff from the TATA book, this is currently underdeveloped in my lecture notes)

using tree automata to solve decision problems: Skolem arithmetic, FO theory of monadic rpo, theory of multiple congruence relations on terms

variations and limitations: problems with having classes of tree automata closed under cylindrification/projection. The special case of automata for monadic logics (the Lille/Orsay school of reduction automata etc.)

Material