TY - JOUR
T1 - Paths, tree homomorphisms and disequalities for H1-clauses
AU - Reuß, Andreas
AU - Seidl, Helmut
N1 - Publisher Copyright:
© Cambridge University Press 2017.
PY - 2018/11/1
Y1 - 2018/11/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85038029226&partnerID=8YFLogxK
U2 - 10.1017/S096012951700024X
DO - 10.1017/S096012951700024X
M3 - Article
AN - SCOPUS:85038029226
SN - 0960-1295
VL - 28
SP - 1786
EP - 1846
JO - Mathematical Structures in Computer Science
JF - Mathematical Structures in Computer Science
IS - 10
ER -