{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,2]],"date-time":"2025-11-02T16:23:26Z","timestamp":1762100606717},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_15","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T21:12:31Z","timestamp":1167426751000},"page":"184-199","source":"Crossref","is-referenced-by-count":6,"title":["Efficient Minimal Model Generation Using Branching Lemmas"],"prefix":"10.1007","author":[{"given":"Ryuzo","family":"Hasegawa","sequence":"first","affiliation":[]},{"given":"Hiroshi","family":"Fujita","sequence":"additional","affiliation":[]},{"given":"Miyuki","family":"Koshimura","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/3-540-61208-4_10","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"F. Bry","year":"1996","unstructured":"Bry, F., Yahya, A.: Minimal Model Generation with Positive Unit Hyper- Resolution Tableaux. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS(LNAI), vol.\u00a01071, pp. 143\u2013159. Springer, Heidelberg (1996)"},{"key":"15_CR2","unstructured":"Bry, F.: (1999), http:\/\/www.pms.informatik.uni-muenchen.de\/software\/MM-SATCHMO\/"},{"issue":"1","key":"15_CR3","first-page":"63","volume":"3","author":"H. Fujita","year":"1998","unstructured":"Fujita, H., Hasegawa, R.: Implementing a Model-Generation Based Theorem Prover MGTP in Java. Research Reports on Information Science and Electrical Engineering of Kyushu University\u00a03(1), 63\u201368 (1998)","journal-title":"Research Reports on Information Science and Electrical Engineering of Kyushu University"},{"issue":"1","key":"15_CR4","first-page":"57","volume":"4","author":"R. Hasegawa","year":"1999","unstructured":"Hasegawa, R., Fujita, H.: A New Implementation Technique for Model Generation Theorem Provers To Solve Constraint Satisfaction Problems. Research Reports on Information Science and Electrical Engineering of Kyushu University\u00a04(1), 57\u201362 (1999)","journal-title":"Research Reports on Information Science and Electrical Engineering of Kyushu University"},{"key":"15_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-55602-8_180","volume-title":"Automated Deduction - CADE-11","author":"K. Inoue","year":"1992","unstructured":"Inoue, K., Koshimura, M., Hasegawa, R.: Embedding Negation as Failure into a Model Generation Theorem Prover. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 400\u2013415. Springer, Heidelberg (1992)"},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"Letz, R., Mayer, K., Goller, C.: Controlled Integration of the Cut Rule into Connection Tableau Calculi. J. of Automated Reasoning\u00a013, 297\u2013337 (1994)","journal-title":"J. of Automated Reasoning"},{"key":"15_CR7","unstructured":"Lu, W.: Minimal Model Generation Based on E-hyper Tableaux. Research reports 20-96 (1996)"},{"key":"15_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1007\/3-540-61208-4_18","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"I. Niemel\u00e4","year":"1996","unstructured":"Niemel\u00e4, I.: A Tableaux Calculus for Minimal Model Reasoning. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS(LNAI), vol.\u00a01071, pp. 278\u2013294. Springer, Heidelberg (1996)"},{"key":"15_CR9","first-page":"249","volume-title":"Proc. of the 12-th Int. Conf. on Logic Programming","author":"Y. Shirai","year":"1995","unstructured":"Shirai, Y., Hasegawa, R.: Two Approaches for Finite-Domain Constraint Satisfaction Problem \u2014 CP and MGTP \u2014. In: Proc. of the 12-th Int. Conf. on Logic Programming, pp. 249\u2013263. MIT Press, Cambridge (1995)"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Stickel, M.: The Path-Indexing Method For Indexing Terms. Technical Note No.473. AI Center, SRI International (1989)","DOI":"10.21236\/ADA460990"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Suttner, C., Yemenis, T.: The TPTP Problem Library. In: Proc. CADE-12, pp. 252\u2013266 (1994)","DOI":"10.1007\/3-540-58156-1_18"},{"key":"15_CR12","doi-asserted-by":"crossref","first-page":"217","DOI":"10.7551\/mitpress\/4298.003.0029","volume-title":"Proc. 12th Int. Conf. on Logic Programming","author":"N. Zhou","year":"1995","unstructured":"Zhou, N.: A Logic Programming Approach to Channel Routing. In: Proc. 12th Int. Conf. on Logic Programming, pp. 217\u2013231. MIT Press, Cambridge (1995)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T17:37:39Z","timestamp":1707500259000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/10721959_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}