{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:27:10Z","timestamp":1725460030053},"publisher-location":"Berlin\/Heidelberg","reference-count":24,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540582770"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0049334","type":"book-chapter","created":{"date-parts":[[2006,3,6]],"date-time":"2006-03-06T18:58:16Z","timestamp":1141671496000},"page":"223-237","source":"Crossref","is-referenced-by-count":4,"title":["A Horn clause that implies an undecidable set of Horn clauses"],"prefix":"10.1007","author":[{"given":"Jerzy","family":"Marcinkowski","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"K. Apt: Logic Programming; in Handbook of Theoretical Computer Science vol B., J. van Leeuwen (ed). 1990."},{"key":"15_CR2","first-page":"73","volume-title":"Lecture Notes in Computer Science, vol 115","author":"C. Beeri","year":"1981","unstructured":"C. Beeri, M.Y. Vardi: The implication problem for data dependencies; Proc. International Coll. on Automata, Languages and Programming 1981, Lecture Notes in Computer Science, vol 115, pp 73\u201385, Springer, Berlin."},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"W. Bibel, S. H\u00f6lldobler and J. W\u00fcrtz: Cycle Unification; in D. Kapur (ed.), Proc. the Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol 607, Springer (June 1992).","DOI":"10.1007\/3-540-55602-8_158"},{"issue":"3","key":"15_CR4","doi-asserted-by":"crossref","first-page":"671","DOI":"10.1137\/0214049","volume":"14","author":"Ashok K. Chandra","year":"1985","unstructured":"A. K. Chandra, M. Y. Vardi: The implication problem for functional and inclusion dependencies is undecidable; SIAM J. Comput. vol 14, No 3, (1985).","journal-title":"SIAM Journal on Computing"},{"key":"15_CR5","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C.L. Chang","year":"1973","unstructured":"C.L. Chang, R.C.T. Lee: Symbolic Logic and Mechanical Theorem Proving; Academic Press, New York, San Francisco, London 1973"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"P. Devienne, P. Leb\u00e9gue and J.C. Routier: Halting Problem of one Binary Horn Clause is undecidable; proc. of STACS 93, Springer, LNCS, vol 665 pp 48\u201358.","DOI":"10.1007\/3-540-56503-5_7"},{"key":"15_CR7","unstructured":"P.Devienne, P.Leb\u00e9gue J.C.Routier:Cycle Unification is Undecidable. prepr.1992"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"G.Gottlob, A.Leitsch:Fast Subsumption Algorithms; LNCS 204-II, Springer, 1985.","DOI":"10.1007\/3-540-15984-3_239"},{"issue":"No.2","key":"15_CR9","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1145\/3149.214118","volume":"32","author":"G. Gottlob","year":"1985","unstructured":"G. Gottlob, A. Leitsch: On the Efficiency of Subsumption Algorithms; JACM vol 32 No. 2 (April 1985), pp. 280\u2013295.","journal-title":"JACM"},{"key":"15_CR10","unstructured":"G. Gottlob, A. Leitsch: Deciding Horn clause implication problem by ordered semantic resolution; Comp. Intelligence II, F. Gardin, G. Mauri, (ed), 1990."},{"key":"15_CR11","first-page":"25","volume":"5","author":"Y.S. Gurevich","year":"1966","unstructured":"Y.S. Gurevich: The problem of equality of words for certain classes of semigroups; (Russian), Algebra i Logika 5,(1966) pp 25\u201335","journal-title":"Algebra i Logika"},{"key":"15_CR12","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0020-0190(93)90210-Z","volume":"496","author":"P. Hanschke","year":"1993","unstructured":"P. Hanschke, J. W\u00fcrtz: Satisfiability of the Smallest Binary Program; Information Processing Letters 496 (1993) pp. 237\u2013241.","journal-title":"Information Processing Letters"},{"key":"15_CR13","unstructured":"C. Herrmann: On the undecidability of implications between embedded multi-valued database dependencies; preprint."},{"key":"15_CR14","first-page":"1073","volume-title":"Formal Models and Semantics","author":"Paris C. KANELLAKIS","year":"1990","unstructured":"P.C. Kanellakis: Elements of Relational Database Theory; in Handbook of Theoretical Computer Science vol B., J. van Leeuwen (ed). 1990."},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"A. Leitsch, Implication Algorithms for Classes of Horn Clauses; Statistik, Informatik und \u00d6konomie, Springer Verlag 1988, pp 172\u2013179.","DOI":"10.1007\/978-3-642-74052-7_14"},{"key":"15_CR16","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":"15_CR17","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 the propositional calculus (abstract); Bulletin of the American Mathematical Society, 55 p. 50 (1949).","journal-title":"Bulletin of the American Mathematical Society"},{"issue":"No2","key":"15_CR18","doi-asserted-by":"crossref","first-page":"186","DOI":"10.2307\/2271899","volume":"40","author":"R. McKenzie","year":"1975","unstructured":"R. McKenzie: On Spectra, and the Negative Solution of the Decision Problem for Identities Having a Finite Nontrivial Model; The Journal of Symbolic Logic, vol 40, No 2 pp 186\u2013195, 1975.","journal-title":"The Journal of Symbolic Logic"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"J. Marcinkowski, L. Pacholski: Undecidability of the Horn Clause Implication Problem; Proc 33rd Annual Symposium on the Foundations of Computer Science (1992). pp. 354\u2013362.","DOI":"10.1109\/SFCS.1992.267755"},{"issue":"3","key":"15_CR20","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1305\/ndjfl\/1093893456","volume":"9","author":"W. E. Singletary","year":"1968","unstructured":"W.E. Singletary: Results Regarding the Axiomatization of Partial Propositional Calculi; Notre Dame Journal of Formal Logic, vol IX, Number 3, 1968.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"15_CR21","doi-asserted-by":"crossref","first-page":"648","DOI":"10.1145\/321784.321792","volume":"20.4","author":"R.B. Stillman","year":"1973","unstructured":"R.B. Stillman: The Concept of Weak Substitution In Theorem-proving; JACM vol.20.4(Oct. 1973), 648\u2013667.","journal-title":"JACM"},{"key":"15_CR22","doi-asserted-by":"publisher","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":"15_CR23","unstructured":"J. W\u00fcrtz: Unifying Cycles; ECAI 1982, B. Neumann ed. pp 60\u201364."},{"key":"15_CR24","first-page":"35","volume":"V","author":"M. K. Yntema","year":"1964","unstructured":"M. K. Yntema: A detailed argument for the Post-Linial theorems; Notre Dame Journal of Formal Logic, vol V, (1964). pp 35\u201351.","journal-title":"Notre Dame Journal of Formal Logic"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0049334.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:55:44Z","timestamp":1607550944000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0049334"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540582770"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/bfb0049334","relation":{},"subject":[]}}