{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:10:52Z","timestamp":1725664252966},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540577850"},{"type":"electronic","value":"9783540483328"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57785-8_128","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:19:13Z","timestamp":1330262353000},"page":"19-32","source":"Crossref","is-referenced-by-count":1,"title":["One binary horn clause is enough"],"prefix":"10.1007","author":[{"given":"Philippe","family":"Devienne","sequence":"first","affiliation":[]},{"given":"Patrick","family":"Leb\u00e8gue","sequence":"additional","affiliation":[]},{"given":"Jean-Christophe","family":"Routier","sequence":"additional","affiliation":[]},{"given":"J\u00f6rg","family":"W\u00fcrtz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1145\/355592.365646","volume":"9","author":"C. B\u00f6hm","year":"1966","unstructured":"B\u00f6hm C., Jacopini G. \u201cFlow diagrams, Turing machines and languages with only two formation rules.\u201d Communications of the Association for Computing Machinery, Vol. 9, pp. 366\u2013371. 1966.","journal-title":"Communications of the Association for Computing Machinery"},{"key":"2_CR2","unstructured":"Bouquard J.L. \u201cLogic programming and Attribute grammars.\u201d Ph.D. Thesis, Orl\u00e9ans 1992."},{"key":"2_CR3","unstructured":"Bratko I. \u201cProlog Programming for Artificial Intelligence\u201d. Addison-Wesley Publishers limited. 1986."},{"key":"2_CR4","unstructured":"William F. Clocksin and Christopher S. Mellish, \u201cProgramming in Prolog\u201d. Springer-Verlag. 1981."},{"key":"2_CR5","unstructured":"Conway J.H. \u201cUnpredictable Iterations.\u201d Proc. 1972 Number Theory Conference. University of Colorado, pp 49\u201352. 1972."},{"key":"2_CR6","first-page":"939","volume":"77","author":"K.L. Clark","year":"1977","unstructured":"Clark K.L., T\u00e4rnlund S.A. \u201cA First Order Theory of Data and Programs.\u201d in Proc. IFIP 77. pp. 939\u2013944. 1977.","journal-title":"Proc. IFIP"},{"key":"2_CR7","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1016\/0304-3975(92)90022-8","volume":"103","author":"M. Dauchet","year":"1992","unstructured":"Dauchet M. \u201cSimulation of Turing Machines by a regular rewrite rule.\u201d Journal of Theoretical Computer Science. n\u2134103. 409\u2013420. 1992.","journal-title":"Journal of Theoretical Computer Science"},{"key":"2_CR8","first-page":"48","volume-title":"LNCS n\u2134665","author":"P. Devienne","year":"1993","unstructured":"Devienne P., Leb\u00e8gue P., Routier J.C. \u201cHalting Problem of One Binary Horn Clause is Undecidable.\u201d Proceedings of STACS'93, LNCS n\u2134665, pp. 48\u201357, Springer-Verlag. W\u00fcrzburg. February 1993."},{"key":"2_CR9","first-page":"250","volume-title":"In proceedings of ILPS'93","author":"P. Devienne","year":"1993","unstructured":"Devienne P., Leb\u00e8gue P., Routier J.C. \u201cThe Emptiness Problem of One Binary Recursive Horn Clause is Undecidable.\u201d In proceedings of ILPS'93, Vancouver. MIT Press. pp 250\u2013265. October 1993."},{"issue":"3","key":"2_CR10","doi-asserted-by":"crossref","first-page":"471","DOI":"10.2307\/2273045","volume":"38","author":"W. Goldfarb","year":"1973","unstructured":"Goldfarb W. and Lewis H.R. \u201cThe decision problem for formulas with a small number of atomic subformulas\u201d J. Symbolic Logic 38(3), pp. 471\u2013480, 1973.","journal-title":"J. Symbolic Logic"},{"key":"2_CR11","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1080\/0025570X.1983.11977011","volume":"n\u213456","author":"R.K. Guy","year":"1983","unstructured":"Guy R.K. \u201c Conway's Prime Producing Machine.\u201d Mathematics Magazine. n\u213456. 26\u201333. 1983.","journal-title":"Mathematics Magazine"},{"issue":"n\u21345","key":"2_CR12","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1016\/0020-0190(93)90210-Z","volume":"45","author":"P. Hanschke","year":"1993","unstructured":"Hanschke P., W\u00fcrtz J. \u201cSatisfiability of the Smallest Binary Program.\u201d Information Processing Letters, vol. 45, n\u21345. pp. 237\u2013241. April 1993.","journal-title":"Information Processing Letters"},{"issue":"n\u21347","key":"2_CR13","doi-asserted-by":"crossref","first-page":"379","DOI":"10.1145\/358886.358892","volume":"23","author":"D. Harel","year":"1980","unstructured":"Harel D. \u201cOn folk theorems\u201d CACM, vol. 23, n\u21347. pp. 379\u2013389. 1980.","journal-title":"CACM"},{"key":"2_CR14","volume-title":"Logic for Problem Solving","author":"R. A. Kowalski","year":"1979","unstructured":"Kowalski R. A. \u201cLogic for Problem Solving.\u201d North Holland. New York. 1979."},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Marcinkowski J., Leszek Pacholski \u201cUndecidability of the Horn-Clause Implication Problem\u201d Proc. of the 33rd FOCS. 1992.","DOI":"10.1109\/SFCS.1992.267755"},{"key":"2_CR16","unstructured":"Minsky M. \u201cComputation: Finite and Infinite Machines.\u201d Prentice-Hall. 1967."},{"key":"2_CR17","series-title":"LOPSTR'91","volume-title":"Logic program synthesis and transformation","author":"A. Parrain","year":"1991","unstructured":"Parrain A., Devienne P., Leb\u00e8gue P. \u201cProlog programs transformations and Meta-Interpreters.\u201d Logic program synthesis and transformation, Springer-Verlag, LOPSTR'91, Manchester. 1991."},{"key":"2_CR18","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"Robinson J. A. \u201cA Machine-oriented Logic Based on the Resolution Principle.\u201d J. ACM n\u2134 12, pp. 23\u201345. Januar 1965.","journal-title":"J. ACM"},{"key":"2_CR19","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/0304-3975(88)90146-6","volume":"n\u213459","author":"M. Schmidt-Schauss","year":"1988","unstructured":"Schmidt-Schauss M. \u201cImplication of clauses is undecidable.\u201d Journal of Theoretical Computer Science, n\u213459, pp. 287\u2013296. 1988.","journal-title":"Journal of Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","STACS 94"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57785-8_128.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:13:51Z","timestamp":1605647631000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57785-8_128"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540577850","9783540483328"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-57785-8_128","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}