{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T15:33:23Z","timestamp":1648568003708},"reference-count":59,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":3855,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[2003,2]]},"DOI":"10.1016\/s0168-0072(02)00032-5","type":"journal-article","created":{"date-parts":[[2002,10,10]],"date-time":"2002-10-10T17:33:13Z","timestamp":1034271193000},"page":"19-59","source":"Crossref","is-referenced-by-count":2,"title":["Thue trees"],"prefix":"10.1016","volume":"119","author":[{"given":"Jerzy","family":"Marcinkowski","sequence":"first","affiliation":[]},{"given":"Leszek","family":"Pacholski","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0168-0072(02)00032-5_BIB1","doi-asserted-by":"crossref","first-page":"638","DOI":"10.1007\/BF01448869","article-title":"\u00dcber die erf\u00fcllbarkeit gewisser z\u00e4hlausdr\u00fccke","volume":"100","author":"Ackermann","year":"1928","journal-title":"Mathematische Annalen"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB2","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/BF01565424","article-title":"Beitr\u00e4ge zum entscheidungsproblem der mathematischen logik","volume":"112","author":"Ackermann","year":"1936","journal-title":"Mathematische Annalen"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB3","series-title":"Solvable Cases of the Decision Problem","author":"Ackermann","year":"1954"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB4","series-title":"Term Rewriting and All That","author":"Baader","year":"1998"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB5","doi-asserted-by":"crossref","unstructured":"C. Beeri, M. Vardi, The implication problem for data dependencies, in: Proc. Internat. Collaq. on Automata, Languages and Programming 1981, Lecture Notes in Computer Science, Vol. 115, Springer, Berlin, 1981, pp. 73\u201385.","DOI":"10.1007\/3-540-10843-2_7"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB6","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/BF01459101","article-title":"Zum entscheidungsproblem der mathematischen logik","volume":"99","author":"Bernays","year":"1928","journal-title":"Mathematische Annalen"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB7","series-title":"Proc. Conf. on Automated Deduction","article-title":"Cycle unification","volume":"Vol. 607","author":"Bibel","year":"1992"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB8","series-title":"Perspectives in Mathematical Logic","article-title":"The classical decision problem","author":"B\u00f6rger","year":"1997"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB9","first-page":"328","article-title":"Encompassment properties and automata with constraint","volume":"Vol. 690","author":"Caron","year":"1993"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB10","doi-asserted-by":"crossref","unstructured":"A. Chandra, H. Lewis, J. Makowsky, Embedded implicational dependencies and their inference problem, in: Proc. 13th Ann. ACM Symp. on Theory of Computing, 1981, pp. 342\u2013354.","DOI":"10.1145\/800076.802488"},{"issue":"3","key":"10.1016\/S0168-0072(02)00032-5_BIB11","doi-asserted-by":"crossref","first-page":"671","DOI":"10.1137\/0214049","article-title":"The implication problem for functional and inclusion dependencies is undecidable","volume":"14","author":"Chandra","year":"1985","journal-title":"SIAM J. Comput."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB12","series-title":"Symbolic Logic and Mechanical Theorem Proving","author":"Chang","year":"1973"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB13","series-title":"Proc. 5th IEEE Lectures in Information and Computer Science","first-page":"242","article-title":"The theory of ground rewrite systems is decidable","author":"Dauchet","year":"1990"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB14","series-title":"Handbook of Mathematical Logic","first-page":"567","article-title":"Unsolvable problems","author":"Davis","year":"1977"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB15","doi-asserted-by":"crossref","unstructured":"N. Dershowitz, J. Jouannaud, J.W. Klop, More problems in rewriting, in: Proc. 5th RTA, Lecture Notes in Computer Science, Vol. 690, Springer, Berlin, 1993, pp. 468\u2013487.","DOI":"10.1007\/3-540-56868-9_39"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB16","doi-asserted-by":"crossref","unstructured":"N. Dershowitz, J. Jouannaud, J.W. Klop, Problems in rewriting iii, in: Proc. RTA, Lecture Notes in Computer Science, Vol. 914, Springer, Berlin, 1995, pp. 457\u2013471.","DOI":"10.1007\/3-540-59200-8_82"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB17","first-page":"1","article-title":"Smallest Horn clause programs","volume":"19","author":"Devienne","year":"1994","journal-title":"J. Logic Program."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB18","doi-asserted-by":"crossref","unstructured":"P. Devienne, P. Leb\u00e9gue, J. Routier, Halting problem of one binary Horn clause is undecidable, in: Proc. 10th Symp. on Theoretical Aspects of Computer Science, STACS\u201993, Lecture Notes in Computer Science, Vol. 665, Springer, Berlin, 1993, pp. 48\u201358.","DOI":"10.1007\/3-540-56503-5_7"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB19","doi-asserted-by":"crossref","unstructured":"P. Devienne, P. Lebegue, J. Routier, J. W\u00fcrtz, One binary Horn clause is enough, in: Proc. 11th Symp. on Theoretical Aspects of Computer Science, STACS\u201994, Lecture Notes in Computer Science, Vol. 775, Springer, Berlin, 1994, pp. 21\u201333.","DOI":"10.1007\/3-540-57785-8_128"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB20","series-title":"The Decision Problem: Solvable Classes of Quantificational Formulas","author":"Dreben","year":"1979"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB21","first-page":"27","article-title":"Ein spezialfall des entscheidungsproblem des theoretischen logik","volume":"2","author":"G\u00f6del","year":"1932","journal-title":"Ergebnisse eines Mathematischen Kolloquims"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB22","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1007\/BF01708881","article-title":"Zum entscheidungsproblem des logischen funktionenkalk\u00fcls","volume":"40","author":"G\u00f6del","year":"1933","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB23","unstructured":"W. Goldfarb, On decision problems for quantification theory. Ph.D. Thesis, Harvard University, 1974 (abstract in Notices Amer. Math. Soc. 21 (4) 280)."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB24","doi-asserted-by":"crossref","first-page":"1237","DOI":"10.2307\/2274274","article-title":"The unsolvability of the G\u00f6del class with identity","volume":"49","author":"Goldfarb","year":"1984","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB25","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/0020-0190(87)90103-7","article-title":"Subsumption and implication","volume":"24","author":"Gottlob","year":"1987","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB26","doi-asserted-by":"crossref","unstructured":"G. Gottlob, A. Leitsch, Fast subsumption algorithms, in: Lecture Notes in Computer Science, Vol. 204-II, Springer, Berlin, 1985, pp. 64\u201377.","DOI":"10.1007\/3-540-15984-3_239"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB27","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1145\/3149.214118","article-title":"On the efficiency of subsumption algorithms","volume":"32","author":"Gottlob","year":"1985","journal-title":"JACM"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB28","first-page":"19","article-title":"Deciding Horn clause implication problems by ordered semantic resolution","volume":"II","author":"Gottlob","year":"1990","journal-title":"Comput. Intell."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB29","doi-asserted-by":"crossref","first-page":"460","DOI":"10.2307\/2272244","article-title":"The decision problem for standard classes","volume":"41","author":"Gurevich","year":"1976","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB30","series-title":"Current Trends in Theoretical Computer Science","first-page":"254","article-title":"On the classical decision problem","author":"Gurevich","year":"1993"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB31","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0020-0190(93)90210-Z","article-title":"Satisfiability of the smallest binary program","volume":"496","author":"Hanschke","year":"1993","journal-title":"Informat. Process. Lett."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB32","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1006\/inco.1995.1148","article-title":"On the undecidability of implications between embedded multivalued database dependencies","volume":"122","author":"Herrman","year":"1995","journal-title":"Inform. Comput."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB33","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/BF01452848","article-title":"\u00dcber die erf\u00fcllbarkeit derjenigen z\u00e4hlausdr\u00fccke, welche in der normalform zwei benachbarte allzeichen enthalten","volume":"108","author":"Kalm\u00e4r","year":"1933","journal-title":"Mathematische Annalen"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB34","article-title":"Elements of relational database theory","volume":"Vol. B","author":"Kanellakis","year":"1990"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB35","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1006\/inco.1993.1003","article-title":"The undecidability of the semiunification problem","volume":"102","author":"Kfoury","year":"1993","journal-title":"Inform. Comput."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB36","doi-asserted-by":"crossref","unstructured":"A. Leitsch, Statistik, Informatik und Okonomie, (chap.), Implication Algorithms for Horn clauses, Springer, Berlin, 1988, pp. 172\u2013189.","DOI":"10.1007\/978-3-642-74052-7_14"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB37","doi-asserted-by":"crossref","unstructured":"A. Leitsch, Deciding Horn clauses by hyperresolution, in: Proc. Computer Science Logic, Lecture Notes in Computer Science, Vol. 440, Springer, Berlin, 1989, pp. 225\u2013241.","DOI":"10.1007\/3-540-52753-2_42"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB38","series-title":"Unsolvable Classes of Quantificational Formulas","author":"Lewis","year":"1979"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB39","doi-asserted-by":"crossref","first-page":"471","DOI":"10.2307\/2273045","article-title":"The decision problem for formulas with a small number of atomic subformulas","volume":"38","author":"Lewis","year":"1973","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB40","doi-asserted-by":"crossref","unstructured":"J. Marcinkowski, A Horn clause that implies an undecidable set of Horn clauses, in: Proc. 1993 Annu. Conf. of the European Association of Computer Science Logic, Lecture Notes in Computer Science, Vol. 832, Springer, Berlin, 1994, pp. 223\u2013237.","DOI":"10.1007\/BFb0049334"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB41","unstructured":"J. Marcinkowski, Undecidability of the Horn clause finite implication problem, Presented during Annu. Conf. on Computer Science Logic in Paderborn, 1995."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB42","doi-asserted-by":"crossref","unstructured":"J. Marcinkowski, Undecidability of the first order theory of one-step right ground rewriting, in: Proc. Rewriting Techniques and Applications, Lecture Notes in Computer Science, Vol. 1232, Springer, Berlin, 1997, pp. 241\u2013253.","DOI":"10.1007\/3-540-62950-5_75"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB43","doi-asserted-by":"crossref","unstructured":"J. Marcinkowski, L. Pacholski, Undecidability of the Horn clause implication problem, in: Proc. 33rd Annu. IEEE Symp. on the Foundations of Computer Science, Los Alamitos, 1992, pp. 354\u2013362.","DOI":"10.1109\/SFCS.1992.267755"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB44","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/0003-4843(76)90009-7","article-title":"The decision problem for equational bases of algebras","volume":"11","author":"McNulty","year":"1976","journal-title":"Ann. Math. Logic"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB45","doi-asserted-by":"crossref","first-page":"589","DOI":"10.2307\/2272037","article-title":"Undecidable properties of finite sets of equations","volume":"41","author":"McNulty","year":"1976","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB46","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1305\/ndjfl\/1093956081","article-title":"Unsolvable problems for equational theories","volume":"8","author":"Perkins","year":"1967","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB47","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2267170","article-title":"Recursive unsolvability of a problem of Thue","volume":"12","author":"Post","year":"1947","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB48","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin","year":"1969","journal-title":"Trans. Amer. Math. Soc."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB49","series-title":"Theory of Recursive Functions and Effective Computability","author":"Rogers","year":"1967"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB50","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0304-3975(88)90146-6","article-title":"Implication of clauses is undecidable","volume":"59","author":"Schmidt-Schau\u00df","year":"1988","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB51","unstructured":"F. Seynhaeve, M. Tommasi, R. Treinen, Grid structures and undecidable properties, in: Proc. TAPSOFT, Lecture Notes in Computer Science, Vol. 1214, Springer, Berlin, 1997, pp. 357\u2013368."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB52","doi-asserted-by":"crossref","first-page":"32","DOI":"10.1007\/BF02759780","article-title":"Decidability of a portion of the predicate calculus","volume":"28","author":"Shelah","year":"1977","journal-title":"Israel J. Math."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB53","first-page":"37","article-title":"Untersuchungen \u00fcber die axiome des klassenkalk\u00fcls und \u00fcber produktations- und summationsprobleme, welche gewisse klassen von aussagen betreffen","volume":"3","author":"Skolem","year":"1919","journal-title":"Skrifter utgit au Vidensk. i. Kristiania I, Math.-nat.Klasse"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB54","unstructured":"T. Skolem, Logisch-kombinatorische untersuchungen \u00fcber die erf\u00fcllbarkeit oder beweisbarkeit mathematischer s\u00e4tze nebst einem theorem \u00fcber dichte mengen, Norsk Vid-Akad. Oslo Mat.-Natur Kl. Skr. 4, 1920."},{"key":"10.1016\/S0168-0072(02)00032-5_BIB55","first-page":"125","article-title":"\u00dcber die mathematische logik","volume":"106","author":"Skolem","year":"1928","journal-title":"Norsk MAt. Tidsskrift"},{"issue":"4","key":"10.1016\/S0168-0072(02)00032-5_BIB56","doi-asserted-by":"crossref","first-page":"648","DOI":"10.1145\/321784.321792","article-title":"The concept of weak substitution in theorem-proving","volume":"20","author":"Stillman","year":"1973","journal-title":"JACM"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB57","doi-asserted-by":"crossref","unstructured":"R. Treinen, The first-order theory of one-step rewriting is undecidable, in: Proc. Rewriting Techniques and Applications, Lecture Notes in Computer Science, Vol. 1103, Springer, Berlin, 1996, pp. 276\u2013285.","DOI":"10.1007\/3-540-61464-8_59"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB58","doi-asserted-by":"crossref","unstructured":"S. Vorobyov, The first-order theory of one step rewriting in linear Noetherian systems is undecidable, in: Proc. Rewriting Techniques and Applications, Lecture Notes in Computer Science, Vol. 1232, Springer, Berlin, 1997, pp. 254\u2013268.","DOI":"10.1007\/3-540-62950-5_76"},{"key":"10.1016\/S0168-0072(02)00032-5_BIB59","unstructured":"H. Wang, Dominoes and the \u2200\u2203\u2200-case of the decision problem, in: Prec. Symp. on Mathematical Theory of Automata, Brooklyn Polytechnic Institute, New York, 1962, pp. 23\u201355."}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007202000325?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007202000325?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,7]],"date-time":"2020-03-07T13:56:14Z","timestamp":1583589374000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0168007202000325"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,2]]},"references-count":59,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2003,2]]}},"alternative-id":["S0168007202000325"],"URL":"https:\/\/doi.org\/10.1016\/s0168-0072(02)00032-5","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[2003,2]]}}}