{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:03Z","timestamp":1749124083133},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_16","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:21:46Z","timestamp":1330269706000},"page":"222-236","source":"Crossref","is-referenced-by-count":3,"title":["Detecting non-provable goals"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Br\u00fcning","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg Verlag, 1987. Second edition.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"16_CR2","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/978-94-011-3488-0_4","volume-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","author":"W. Bibel","year":"1991","unstructured":"W. Bibel. Perspectives on automated deduction. In Automated Reasoning: Essays in Honor of Woody Bledsoe, pages 77\u2013104. Kluwer Academic, Utrecht, 1991."},{"key":"16_CR3","volume-title":"Deduction: Automated Logic","author":"W. Bibel","year":"1993","unstructured":"W. Bibel. Deduction: Automated Logic. Academic Press, London, 1993."},{"key":"16_CR4","first-page":"94","volume-title":"Cycle unification","author":"W. Bibel","year":"1992","unstructured":"W. Bibel, S. H\u00f6lldobler, and J. W\u00fcrtz. Cycle unification. Proceedings of the Conference on Automated Deduction, pages 94\u2013108. Springer, Berlin, 1992."},{"key":"16_CR5","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0304-3975(91)90004-L","volume":"86","author":"R. N. Bol","year":"1991","unstructured":"R. N. Bol, K. R. Apt, and J. W. Klop. An analysis of loop checking mechanisms for logic programming. Theoretical Computer Science, 86:35\u201379, 1991.","journal-title":"Theoretical Computer Science"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"S. Br\u00fcning. Detecting Non-Provable Goals. Technical report, FG Intellektik, FB Informatik, TH Darmstadt, 1993.","DOI":"10.1007\/3-540-58156-1_16"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"S. Br\u00fcning. Search Space Pruning by Checking Dynamic Term Growth. Proceedings of the International Conference on Logic Programming and Automated Reasoning, pages 52\u201363. Springer, 1993.","DOI":"10.1007\/3-540-56944-8_41"},{"key":"16_CR8","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1016\/S0747-7171(85)80027-4","volume":"1","author":"E. Eder","year":"1985","unstructured":"E. Eder. Properties of substitutions and unifications. Journal of Symbolic Computation, 1:31\u201346, 1985.","journal-title":"Journal of Symbolic Computation"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"C. Ferm\u00fcller, A. Leitsch, T. Tammet, and N. Zamov. Resolution Methods for the Decision Problem. LNAI 679. Springer, 1993.","DOI":"10.1007\/3-540-56732-1"},{"issue":"5","key":"16_CR10","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 and J. W\u00fcrtz. Satisfiability of the smallest binary program. Information Processing Letters, 45(5):237\u2013241, April 1993.","journal-title":"Information Processing Letters"},{"key":"16_CR11","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/0743-1066(92)90032-X","volume":"13","author":"G. Janssens","year":"1992","unstructured":"G. Janssens and M. Bruynooghe. Deriving Descriptions of Possible Values of Program Variables by Means of Abstract Interpretation. Journal of Logic Programming, 13:205\u2013258, 1992.","journal-title":"Journal of Logic Programming"},{"key":"16_CR12","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO \u2014 A High-Performance Theorem Prover for First-Order Logic. Journal of Automated Reasoning, 8:183\u2013212, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"J. W. Lloyd. Foundations of Logic Programming. Springer, second edition, 1987.","DOI":"10.1007\/978-3-642-83189-8"},{"key":"16_CR14","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D. W. Loveland","year":"1986","unstructured":"D. W. Loveland. Mechanical theorem proving by model elimination. Journal of the ACM, 15:236\u2013251, 1986.","journal-title":"Journal of the ACM"},{"key":"16_CR15","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/0004-3702(81)90015-1","volume":"16","author":"D. A. Plaisted","year":"1981","unstructured":"D. A. Plaisted. Theorem Proving with Abstraction. Artificial Intelligence, 16:47\u2013108, 1981.","journal-title":"Artificial Intelligence"},{"issue":"1","key":"16_CR16","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23\u201341, 1965.","journal-title":"Journal of the ACM"},{"key":"16_CR17","unstructured":"B. Selman and H. Kautz. Knowlede Compilation Using Horn Approximations. In Proceedings of the AAAI National Conference on Artificial Intelligence, 1991."},{"key":"16_CR18","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/0004-3702(86)90003-2","volume":"30","author":"D. E. Smith","year":"1986","unstructured":"D. E. Smith, M. R. Genesereth, and M. L. Ginsberg. Controlling recursive inference. Artificial Intelligence, 30:343\u2013389, 1986.","journal-title":"Artificial Intelligence"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"M. E. Stickel. A Prolog technology theorem prover. 10th International Conference on Automated Deduction, pages 673\u2013674, Springer, 1990.","DOI":"10.1007\/3-540-52885-7_136"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe. Linear-Input Subset Analysis. Proceedings of the Conference on Automated Deduction, pages 268\u2013280. Springer, 1992.","DOI":"10.1007\/3-540-55602-8_171"},{"key":"16_CR21","unstructured":"D. A. de Waal and J. Gallagher. Logic program specialisation with deletion of useless clauses (poster abstract). Proceedings of the 1993 Logic programming Syposium, page 632, MIT Press,1993."},{"key":"16_CR22","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/0743-1066(91)80002-U","volume":"10","author":"E. Yardeni","year":"1991","unstructured":"E. Yardeni and E. Shapiro. A Type System for Logic Programs. Journal of Logic Programming, 10:125\u2013153, 1991.","journal-title":"Journal of Logic Programming"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T18:39:35Z","timestamp":1687286375000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}