Andreas Reuß and Helmut Seidl. Crossing the Syntactic Barrier: Hom-Disequalities for H1-Clauses. In Nelma Moreira and Rogério Reis, editors, CIAA, pages 301-312, 2012. Springer, LNCS 7381.

We extend H1-clauses with disequalities between images of terms under a tree homomorphism (hom-disequalities). This extension allows to test whether two terms are distinct modulo a semantic interpretation, allowing, e.g., to neglect information that is not considered relevant for the intended comparison. We prove that H1-clauses with hom-disequalities are more expressive than H1-clauses with ordinary term disequalities, and that they are incomparable with H1-clauses with disequalities between paths. Our main result is that H1-clauses with this new type of constraints can be normalized into an equivalent tree automaton with hom-disequalities. Since emptiness for that class of automata turns out to be decidable, we conclude that satisfiability is decidable for positive Boolean combinations of queries to predicates defined by H1-clauses with hom-disequalities.

Reference: Bibtex