Proofs and reachability problem for ground rewrite systems
Résumé
The different reachability problems for ground rewrite systems are decidable[OY86], [DEGI89]. We prove these results using ground tree transducers of [DATI85] and wellknown algorithms on recognizable tree languages in order to obtain efficient algorithms. We introduce and study derivation proofs to describe the sequences of rules used to reduce a term t in a term t' for a given ground rewrite system S and sketch how compute a derivation proof in linear time. Moreover, we study the same problem for recognizable tree languages.