Tree Extension Algebras: Logics, Automata, and Query Languages

We study relations on trees defined by first-order constraints over a vocabulary that includes the tree extension relation Ì Ì ¼, holding if and only if every branch of Ì extends to a branch of Ì ¼, unary node-tests, and a binary relation checking if the domains of two trees are equal. We show that from such a formula one can generate a tree automaton that accepts the set of tuples of trees defined by the formula, and conversely that every automaton over tree-tuples is captured by such a formula. We look at the fragment with only extension inequalities and leaf tests, and show that it corresponds to a new class of automata on tree tuples, which is strictly weaker then general tree-tuple automata. We use the automata representations to show separation and expressibility results for formulae in the logic. We then turn to relational calculi over the logic defined here: that is, from constraints we extend to queries that have second-order parameters for a finite set of tree tup...

• Type: Conference
• Year: 2002
• Where: LICS
• Authors: Michael Benedikt, Leonid Libkin
• Keywords: Automated Reasoning, LICS 2002, Query Evaluation, Tree, Tree Extension