We describe multitree automata and a related logic on multitrees. Multitrees are extensions of trees with both associative and associative-commutative symbols that may bear arbitrary numbers of sons. An originality of our approach is that transitions of an automaton are restricted using Presburger’s constraints. The benefit of this extension is that we generalize, all together, automata with equality and disequalities constraints as well as counting constraints. This new class of automata appears very general as it may encompass hedge automata, a simple yet effective model for XML schemata, feature tree automata, automata with constraints between brothers and automata with arithmetical constraints. Moreover, the class of recognizable languages enjoys all the typical good properties of traditional regular languages: closure under boolean operations and composition by associative and associative-commutative operators, determinisation, decidability of the test for emptiness, …
We apply our automata to query languages for XML-like documents and to automated inductive theorem proving based on rewriting, obtaining each time new results. Using a classical connection between logic and automata, we design a decidable logic for (multi)trees that can be used as a foundation for querying XML-like document. This proposition has the same flavour as a query language for semi-structured recently proposed by Cardelli and Ghelli. The same tree logic is used to yield decidable cases of inductive reducibility modulo associativity-commutativity, a key property in inductive theorem proving based on rewriting.