{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:22Z","timestamp":1749125182793},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_105","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:51:00Z","timestamp":1330293060000},"page":"433-447","source":"Crossref","is-referenced-by-count":7,"title":["Efficient model generation through compilation"],"prefix":"10.1007","author":[{"given":"Heribert","family":"Sch\u00fctz","sequence":"first","affiliation":[]},{"given":"Tim","family":"Geisler","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"42_CR1","doi-asserted-by":"crossref","unstructured":"F. Bancilhon and R. Ramakrishnan. An amateur's introduction to recursive query processing strategies. In Proc. ACM SIGMOD 1986, pages 16\u201352. ACM, 1986.","DOI":"10.1145\/16894.16859"},{"key":"42_CR2","unstructured":"R. Bayer. Query evaluation and recursion in deductive database systems. Technical Report TUM-I8503, Technische Universit\u00e4t M\u00fcnchen, 1985."},{"key":"42_CR3","doi-asserted-by":"crossref","unstructured":"F. Bry and A. Yahya. Minimal model generation with positive unit hyper-resolution tableaux. In 5th Workshop on Theorem Proving with Tableaux and Related Methods, Springer LNAI, 1996.","DOI":"10.1007\/3-540-61208-4_10"},{"issue":"1","key":"42_CR4","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/0004-3702(82)90020-0","volume":"19","author":"C. Forgy","year":"1982","unstructured":"C. Forgy. Rete: A fast algorithm for the many patterns\/many objects pattern match problem. Artificial Intelligence, 19(1):17\u201337, 1982.","journal-title":"Artificial Intelligence"},{"key":"42_CR5","unstructured":"H. Fujita and R. Hasegawa. A model generation theorem prover in KL1 using a ramified-stack algorithm. In Logic Programming, Proc. of the 8th Int. Conf., pages 535\u2013548, 1991."},{"key":"42_CR6","doi-asserted-by":"crossref","unstructured":"C. Goller, R. Letz, K. Mayr, and J. Schumann. SETHEO V3.2: Recent devleopments. In Automated Deduction \u2014 CADE-12, Springer LNAI 814, pages 778\u2013782, 1994.","DOI":"10.1007\/3-540-58156-1_59"},{"key":"42_CR7","unstructured":"Institute for New Generation Computer Technology. Model Generation Theorem Prover: MGTP, 1995. http:\/\/www.icot.or.jp\/ICOT\/IFS\/IFS-abst\/082.html."},{"key":"42_CR8","first-page":"415","volume":"310","author":"R. Manthey","year":"1988","unstructured":"R. Manthey and F. Bry. SATCHMO: A theorem prover implemented in Prolog. In 9th Int. Conf. on Automated Deduction (CADE), Springer LNCS 310, pages 415\u2013434, 1988.","journal-title":"Springer LNCS"},{"key":"42_CR9","doi-asserted-by":"crossref","unstructured":"W. W. McCune. Otter 3.0 reference manual and guide. Technical Report ANL 94\/6, Argonne National Laboratory, 1994.","DOI":"10.2172\/10129052"},{"key":"42_CR10","unstructured":"D. Sahlin. An Automatic Partial Evaluator for Full Prolog. SICS Dissertation Series 04, The Royal Institute of Technology (KTH), 1991."},{"key":"42_CR11","unstructured":"H. Sch\u00fctz. Tuple-oriented Bottom-up Evaluation of Logic Programs. PhD thesis, Technische Universit\u00e4t M\u00fcnchen, 1993. in German."},{"key":"42_CR12","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"M. E. Stickel. A Prolog technology theorem prover: Implementation by an extended Prolog compiler. Journal of Automated Reasoning, 4:353\u2013380, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"42_CR13","first-page":"252","volume":"814","author":"G. Sutcliffe","year":"1994","unstructured":"G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In Automated Deduction \u2014 CADE-12, Springer LNAI 814, pages 252\u2013266, 1994.","journal-title":"Springer LNAI"},{"key":"42_CR14","doi-asserted-by":"crossref","unstructured":"J. E. Wunderwald. Memoing evaluation by source-to-source transformation. In Fifth Int. Workshop on Logic Program Synthesis and Transformation, 1995.","DOI":"10.1007\/3-540-60939-3_2"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_105.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:13Z","timestamp":1605647233000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_105"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_105","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}