{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:20:59Z","timestamp":1747592459926},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540527534"},{"type":"electronic","value":"9783540471370"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1990]]},"DOI":"10.1007\/3-540-52753-2_42","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T21:42:10Z","timestamp":1330206130000},"page":"225-241","source":"Crossref","is-referenced-by-count":7,"title":["Deciding Horn classes by hyperresolution"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Leitsch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"14_CR1","unstructured":"C. L. Chang & R. C. T. Lee: Symbolic Logic and Mechanical Theorem Proving, Academic Press 1973."},{"key":"14_CR2","unstructured":"B. Dreben & W. D. Goldfarb: The Decision Problem \u2014 Solvable Classes of Quantificational Formulas, Addison Wesley 1979."},{"key":"14_CR3","unstructured":"C.Ferm\u00fcller: Deciding some Horn Clause Sets by Resolution, to appear in the Yearbook of the Kurt G\u00f6del Society 1989."},{"key":"14_CR4","volume-title":"Computers and Intractability","author":"M. R. Garey","year":"1979","unstructured":"M. R. Garey & D. S. Johnson: Computers and Intractability; Freeman & Comp., San Francisco, 1979."},{"key":"14_CR5","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/0020-0190(87)90103-7","volume":"24","author":"G. Gottlob","year":"1987","unstructured":"G. Gottlob: Subsumption and Implication, Information Processing Letters 24 (1987), 109\u2013111.","journal-title":"Information Processing Letters"},{"issue":"3","key":"14_CR6","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W. H. Joyner Jr.","year":"1976","unstructured":"W. H. Joyner jr.: Resolution Strategies as Decision Procedures, JACM Vol 23 No. 3, (July 1976), 398\u2013417.","journal-title":"JACM"},{"key":"14_CR7","first-page":"172","volume-title":"Implication Algorithms for Classes of Horn Clauses, Statistik, Informatik + Oekonomie","author":"A. Leitsch","year":"1988","unstructured":"A. Leitsch: Implication Algorithms for Classes of Horn Clauses, Statistik, Informatik + Oekonomie, Springer Verl. Berlin, Heidelberg, 1988, 172\u2013189."},{"key":"14_CR8","unstructured":"A.Leitsch, G.Gottlob: Deciding Horn Clause Implication by Ordered Semantic Resolution, to appear in Proc. Intern. Symp. Computational Intelligence 89, Elsevier 1989."},{"key":"14_CR9","unstructured":"H.R. Lewis: Unsolvable Classes of Quantificational Formulas, Addison Wesley 1979."},{"key":"14_CR10","unstructured":"D. Loveland: Automated Theorem Proving \u2014 A Logical Basis, North Holland Publ. Comp. 1978."},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"A. Martelli, U. Montanari: An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems, Vol. 4 No. 2, (April 1982).","DOI":"10.1145\/357162.357169"},{"key":"14_CR12","first-page":"1","volume":"170","author":"J. Siekmann","year":"1984","unstructured":"J. Siekmann: Universal Unification, 7th International Conference on Automated Deduction, LNCS 170(1984),1\u201342.","journal-title":"LNCS"},{"key":"14_CR13","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), 287\u2013296.","journal-title":"Theoretical Computer Science"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"S. Stenlund: Combinators, \u03bb-Terms and Proof Theory, Reidel Publ. Comp. 1971.","DOI":"10.1007\/978-94-010-2913-1"}],"container-title":["Lecture Notes in Computer Science","CSL '89"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-52753-2_42.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:25:10Z","timestamp":1605648310000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-52753-2_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1990]]},"ISBN":["9783540527534","9783540471370"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-52753-2_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1990]]}}}