Andreas Reuß and Helmut Seidl. Paths, Tree Homomorphisms, and Disequalities for H1-Clauses. Mathematical Structures in Computer Science, :1--61, 2017.
It is well-known that satisfiability is decidable for Horn clauses of the class H1. Since arbitrary Horn clauses can naturally be approximated by H1-clauses, H1 can be used for realizing any program analysis which can be specified by means of Horn clauses. Recently, we have shown that decidability for Horn clauses from H1 is retained if the clauses are either extended with tests for disequality between subterms identified by paths or for disequality between homomorphic images of terms. These two results refer to orthogonal extensions of H1-clauses. Here, we provide a generalization of both results. For that, we introduce hom-path disequalities and show that for each finite set of H1-clauses extended with such tests an equivalent tree automaton with hom-path disequalities can be constructed. Since emptiness for that class of automata has been shown decidable by Godoy et al. in 2010, we conclude that satisfiability is decidable for H1-clauses with hom-path disequalities.