{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T06:04:59Z","timestamp":1649052299187},"reference-count":17,"publisher":"Cambridge University Press (CUP)","issue":"10","license":[{"start":{"date-parts":[[2017,12,6]],"date-time":"2017-12-06T00:00:00Z","timestamp":1512518400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2018,11]]},"abstract":"It is well known that satisfiability is decidable for Horn clauses of the class <\/jats:private-char>. Since arbitrary Horn clauses can naturally be approximated by <\/jats:private-char>-clauses, <\/jats:private-char> 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 <\/jats:private-char> 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 <\/jats:private-char>-clauses. Here, we provide a generalization of both results. For that, we introduce hom-path disequalities and show that for each finite set of <\/jats:private-char>-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 <\/jats:private-char>-clauses with hom-path disequalities.<\/jats:p>","DOI":"10.1017\/s096012951700024x","type":"journal-article","created":{"date-parts":[[2017,12,6]],"date-time":"2017-12-06T07:05:13Z","timestamp":1512543913000},"page":"1786-1846","source":"Crossref","is-referenced-by-count":0,"title":["Paths, tree homomorphisms and disequalities for -clauses"],"prefix":"10.1017","volume":"28","author":[{"given":"ANDREAS","family":"REU\u00df","sequence":"first","affiliation":[]},{"given":"HELMUT","family":"SEIDL","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2017,12,6]]},"reference":[{"key":"S096012951700024X_ref11","first-page":"20","volume-title":"SAS","author":"Nielson","year":"2002"},{"key":"S096012951700024X_ref9","first-page":"363","volume-title":"VMCAI","author":"Goubault-Larrecq","year":"2005"},{"key":"S096012951700024X_ref6","first-page":"244","volume-title":"AUSCRYPT","author":"Fujioka","year":"1993"},{"key":"S096012951700024X_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2005.04.007"},{"key":"S096012951700024X_ref7","first-page":"485","volume-title":"STOC","author":"Godoy","year":"2010"},{"key":"S096012951700024X_ref1","doi-asserted-by":"publisher","DOI":"10.1145\/1324249.1324261"},{"key":"S096012951700024X_ref5","first-page":"314","volume-title":"LICS","author":"Fr\u00fchwirth","year":"1991"},{"key":"S096012951700024X_ref14","first-page":"484","volume-title":"CSL","author":"Seidl","year":"1999"},{"key":"S096012951700024X_ref16","first-page":"165","volume-title":"FoSSaCS","author":"Seidl","year":"2012"},{"key":"S096012951700024X_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2011.07.011"},{"key":"S096012951700024X_ref3","first-page":"151","volume-title":"STACS","author":"Comon","year":"1994"},{"key":"S096012951700024X_ref4","first-page":"255","volume-title":"LICS","author":"Creus","year":"2012"},{"key":"S096012951700024X_ref12","first-page":"581","volume-title":"LPAR-17","author":"Reu\u00df","year":"2010"},{"key":"S096012951700024X_ref2","first-page":"82","volume-title":"CSFW","author":"Blanchet","year":"2001"},{"key":"S096012951700024X_ref10","first-page":"79","volume-title":"VMCAI","author":"M\u00fcller-Olm","year":"2005"},{"key":"S096012951700024X_ref17","first-page":"314","volume-title":"CADE","author":"Weidenbach","year":"1999"},{"key":"S096012951700024X_ref13","first-page":"301","volume-title":"CIAA","author":"Reu\u00df","year":"2012"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012951700024X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,12]],"date-time":"2019-04-12T22:46:09Z","timestamp":1555109169000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012951700024X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,6]]},"references-count":17,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2018,11]]}},"alternative-id":["S096012951700024X"],"URL":"https:\/\/doi.org\/10.1017\/s096012951700024x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,6]]}}}