Paramodulation based procedures for extended tree automata.

equality constraints, a tree memory or computation modulo equational theories
(or also arbitrary combinations of these features).
Such classes of extended tree automata have shwon a good potential 
for application in software and protocol verification. 
The representation of tree automata as Horn clauses
offers a unified framework for defining such extensions.
Moreover, in this settings, problems such as the emptiness 
of the recognized language can be shown decidable 
by proving that the saturation of tree automata presentations 
with suitable paramodulation strategies terminates. 
Alternatively these results can be viewed as new decidable classes of first-order formula.