Name
Abstract | ||
|---|---|---|
We extend ${\mathcal H}_1$-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 ${\mathcal H}_1$-clauses with hom-disequalities are more expressive than ${\mathcal H}_1$-clauses with ordinary term disequalities, and that they are incomparable with ${\mathcal H}_1$-clauses with disequalities between paths. Our main result is that ${\mathcal H}_1$-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 ${\mathcal H}_1$-clauses with hom-disequalities. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-31606-7_26 | CIAA |
Keywords | DocType | Citations |
main result,mathcal H,positive Boolean combination,intended comparison,syntactic barrier,new type,distinct modulo,tree homomorphism,ordinary term disequalities,neglect information,equivalent tree automaton | Conference | 0 |
PageRank | References | Authors |
0.34 | 9 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andreas Reuß | 1 | 2 | 1.46 |
| Helmut Seidl | 2 | 1468 | 103.61 |