{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:14:13Z","timestamp":1725455653989},"publisher-location":"Berlin\/Heidelberg","reference-count":19,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540571841"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0022554","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T01:14:45Z","timestamp":1131844485000},"page":"63-68","source":"Crossref","is-referenced-by-count":0,"title":["Undecidability of implication problems in logic programming, database theory and classical logic"],"prefix":"10.1007","author":[{"given":"Leszek","family":"Pacholski","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/3-540-10843-2_7","volume":"115","author":"C. Beeri","year":"1981","unstructured":"C. Beeri, M. Vardi, The Implication Problem for Data Dependencies, Proc. 8th ICALP, Lecture Notes in Computer Science 115, (1981), pp. 73\u201385.","journal-title":"Lecture Notes in Computer Science"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"W. Bibel, S. H\u00f6lldobler, J. W\u00fcrtz, Cycle Unification, in D. Kapur (ed.), Proceedings of the Conference on Automated Deduction, Lecture Notes on Artificial Intelligence, vol. 607 (1992).","DOI":"10.1007\/3-540-55602-8_158"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"P. Devienne, P. Leb\u00e9gue, J.C. Routier, Halting problem of one binary Horn clause is undecidable, Proceedings of Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science, vol. 665 (1993).","DOI":"10.1007\/3-540-56503-5_7"},{"key":"8_CR4","unstructured":"P. Devienne, P. Leb\u00e9gue, J.C. Routier, Cycle unification is undecidable, unpublished manuscript."},{"key":"8_CR5","doi-asserted-by":"crossref","first-page":"671","DOI":"10.1137\/0214049","volume":"14","author":"A. Chandra","year":"1985","unstructured":"A. Chandra, M. Vardi, The implication problem for functional and inclusion dependencies is undecidable, SIAM Journal of Computing 14 (1985), pp. 671\u2013677.","journal-title":"SIAM Journal of Computing"},{"key":"8_CR6","first-page":"140","volume":"42","author":"Y. Gurevich","year":"1990","unstructured":"Y. Gurevich, On the Classical Decision Problem, Bulletin of European Association for Theoretical Computer Science 42 (1990), pp. 140\u2013150.","journal-title":"Bulletin of European Association for Theoretical Computer Science"},{"key":"8_CR7","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0020-0190(93)90210-Z","volume":"45","author":"P. Hanschke","year":"1993","unstructured":"P. Hanschke, J. W\u00fcrtz, Satisfiability of the smallest binary program, Information Processing Letters 45 (1993), pp.237\u2013241.","journal-title":"Information Processing Letters"},{"key":"8_CR8","unstructured":"G.G. Hillebrand, P.C. Kanellakis, H.G. Mairson, M.Y. Vardi, Undecidable boundedness problems for Datalog programs, to appear."},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"A.J. Kfoury, J. Tiuryn, P. Urzyczyn, The undecidability of the semiunification problem, Proc. 22-nd ACM Symposium on Theory of Computing, Baltimore 1990, pp. 468\u2013476.","DOI":"10.1145\/100216.100279"},{"key":"8_CR10","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/3-540-52753-2_42","volume":"440","author":"A. Leitsch","year":"1989","unstructured":"A. Leitsch, Deciding Horn clauses by hyperresolution, Proc. Computer Science Logic 89, Lecture Notes in Computer Science 440 (1989), pp. 225\u2013241.","journal-title":"Lecture Notes in Computer Science"},{"key":"8_CR11","unstructured":"A. Leitsch, G.Gottlob, Deciding Horn clause implication problems by ordered semantic resolution, Computational Intelligence II, F. Gardin and G. Mauri, ed., 1990, pp.19\u201326."},{"key":"8_CR12","doi-asserted-by":"crossref","first-page":"471","DOI":"10.2307\/2273045","volume":"38","author":"H.R. Lewis","year":"1973","unstructured":"H.R. Lewis, W. Goldfarb, The decision problem for formulas with a small number of atomic subformulas, Journal of Symbolic Logic 38 (1973), pp. 471\u2013480.","journal-title":"Journal of Symbolic Logic"},{"key":"8_CR13","first-page":"50","volume":"55","author":"S. Linial","year":"1949","unstructured":"S. Linial, E. Post, Recursive unsolvability of the deducibility, Tarski's completeness and independence of axioms problems of propositional calculus, Bull. Amer. Math. Soc, vol 55, 1949, p. 50","journal-title":"Bull. Amer. Math. Soc"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"J. Marcinkowski, L. Pacholski, Undecidability of the Horn clause implication problem, Proceedings of 33rd Annual IEEE Symposium on Foundations of Computer Science, Los Alamitos 1992, pp. 354\u2013362.","DOI":"10.1109\/SFCS.1992.267755"},{"key":"8_CR15","unstructured":"J. Marcinkowski, A Horn clause that implies an undecidable set of Horn clauses, to appear."},{"key":"8_CR16","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1016\/0003-4843(76)90009-7","volume":"11","author":"G.F. Mcnulty","year":"1976","unstructured":"G.F. Mcnulty, The decision problem for equational bases of algebras, Annals of Mathematical Logic 11 (1976), pp. 193\u2013259.","journal-title":"Annals of Mathematical Logic"},{"key":"8_CR17","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1016\/S0019-9958(83)80002-3","volume":"56","author":"J.C. Mitchell","year":"1983","unstructured":"J.C. Mitchell, The implication problem for functional and inclusion dependencies, Information and Control 56 (1983), pp 154\u2013173.","journal-title":"Information and Control"},{"key":"8_CR18","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0304-3975(88)90146-6","volume":"59","author":"M. Schmidt-Schauss","year":"1988","unstructured":"M. Schmidt-Schauss, Implication of Clauses is Undecidable, Theoretical Computer Science 59 (1988), pp. 287\u2013296.","journal-title":"Theoretical Computer Science"},{"key":"8_CR19","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1305\/ndjfl\/1093893456","volume":"9","author":"W. Singletary","year":"1968","unstructured":"W. Singletary, Results regarding the axiomatization of partial propositional calculi, Notre Dame J. of Formal Logic, vol. 9 (1968), pp. 193\u2013221.","journal-title":"Notre Dame J. of Formal Logic"}],"container-title":["Lecture Notes in Computer Science","Computational Logic and Proof Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0022554.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T16:48:57Z","timestamp":1607532537000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0022554"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540571841"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0022554","relation":{},"subject":[]}}