{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,6]],"date-time":"2022-04-06T02:15:53Z","timestamp":1649211353787},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2007,7,1]],"date-time":"2007-07-01T00:00:00Z","timestamp":1183248000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Comput Sci Technol"],"published-print":{"date-parts":[[2007,7]]},"DOI":"10.1007\/s11390-007-9062-2","type":"journal-article","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T01:24:26Z","timestamp":1189733066000},"page":"541-553","source":"Crossref","is-referenced-by-count":0,"title":["An Improvement of Herbrand's Theorem and Its Application to Model Generation Theorem Proving"],"prefix":"10.1007","volume":"22","author":[{"given":"Yu-Yan","family":"Chao","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Li-Feng","family":"He","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tsuyoshi","family":"Nakamura","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zheng-Hao","family":"Shi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kenji","family":"Suzuki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hidenori","family":"Itoh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,9,13]]},"reference":[{"key":"9062_CR1","unstructured":"Herbrand J. Recherches sur la th\u00e9orie de la d\u00e9monstration [Dissertation]. University of Paris, 1930."},{"key":"9062_CR2","doi-asserted-by":"crossref","unstructured":"Gilmore P C. A proof method for quantification theory: Its justification and realization. IBM J. Res. Develop. 1960, pp.28~35.","DOI":"10.1147\/rd.41.0028"},{"key":"9062_CR3","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"Proc. 9th Int. Conf. Automated Deduction","author":"R Manthey","year":"1988","unstructured":"Manthey R, Bry F. SATCHMO: A theorem prover implemented in Prolog. In Proc. 9th Int. Conf. Automated Deduction, Argonne, Illinois, USA, 1988, pp.415~434."},{"issue":"1","key":"9062_CR4","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1023\/A:1006291616338","volume":"25","author":"F Bry","year":"2000","unstructured":"Bry F, Yahya A. Positive unit hyperresolution tableaux and their application to minimal model generation. J. Automated Reasoning, 2000, 25(1): 35~82.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"9062_CR5","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BF00881955","volume":"13","author":"M E Stickel","year":"1994","unstructured":"Stickel M E. Upside-down meta-interpretation of the model elimination theorem-proving procedure for deduction and abduction. J. Automated Reasoning, 1994, 13(2): 189~210.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"9062_CR6","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1023\/A:1005851801356","volume":"18","author":"T Geisler","year":"1997","unstructured":"Geisler T, Panne S, Schutz H. Satchmo: The compiling and functional variants. J. Automated Reasoning, 1997, 18(2): 227~236.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"9062_CR7","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1007\/BF00881861","volume":"14","author":"D W Loveland","year":"1995","unstructured":"Loveland D W, Reed D W, Wilson D S. SATCHMORE: SATCHMO with RElevancy. J. Automated Reasoning, 1995, 14(2): 325~351.","journal-title":"J. Automated Reasoning"},{"issue":"1","key":"9062_CR8","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/BF03037320","volume":"16","author":"L He","year":"1998","unstructured":"He L, Chao Y, Simajiri Y et al. $ {\\user1{\\mathcal{A}}} $ -SATCHMORE: SATCHMORE with availability checking. New Generation Computing, 1998, 16(1): 55~74.","journal-title":"New Generation Computing"},{"issue":"3","key":"9062_CR9","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1023\/A:1017594402123","volume":"27","author":"L He","year":"2001","unstructured":"He L. I-SATCHMO: An Improvement of SATCHMO. J. Automated Reasoning, 2001, 27(3): 313~322.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"9062_CR10","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/BF02948883","volume":"18","author":"L He","year":"2003","unstructured":"He L, Chao Y, Nakamura T et al. $ {\\user1{\\mathcal{I}}} $ -SATCHMORE: An improvement of $ {\\user1{\\mathcal{A}}} $ -SATCHMORE. J. Comput. Sci. & Technol., 2003, 18(2): 181~189.","journal-title":"J. Comput. Sci. & Technol."},{"issue":"2","key":"9062_CR11","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1093\/logcom\/14.2.117","volume":"14","author":"L He","year":"2004","unstructured":"He L, Chao Y, Itoh H. R-SATCHMO: Refinements on I-SATCHMO. J. Logic and Computation, 2004, 14(2): 117~143.","journal-title":"J. Logic and Computation"},{"issue":"3","key":"9062_CR12","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/BF03037473","volume":"21","author":"D W Loveland","year":"2003","unstructured":"Loveland D W, Yahya A H. SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy. New Generation Computing, 2003, 21(3): 175~206.","journal-title":"New Generation Computing"},{"key":"9062_CR13","unstructured":"Schulz S. A comparison of different techniques for grounding near-propositional CNF formulae. In Proc. the 15th FLAIRS, London, 2002, pp.72~76."},{"issue":"1","key":"9062_CR14","first-page":"25","volume":"9","author":"S J Lee","year":"1992","unstructured":"Lee S J, Plaisted D A. Eliminating duplication with the hyper-linking strategy. J. Automated Reasoning, 1992, 9(1): 25~42.","journal-title":"J. Automated Reasoning"},{"issue":"3\/4","key":"9062_CR15","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1023\/A:1018976510663","volume":"23","author":"Q Yu","year":"1998","unstructured":"Yu Q, Almulla M, Newborn M. Heuristics used by HERBY for semantic tree theorem proving. Ann. Math. Artif. Intell., 1998, 23(3\/4): 247~266.","journal-title":"Ann. Math. Artif. Intell."},{"key":"9062_CR16","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C L Chang","year":"1997","unstructured":"Chang C L, Lee K C T. Symbolic Logic and Mechanical Theorem Proving. New York: Academic Press, 1997."},{"key":"9062_CR17","volume-title":"Automated Theorem Proving: A Logic Basis","author":"D W Loveland","year":"1978","unstructured":"Loveland D W. Automated Theorem Proving: A Logic Basis. Amsterdam: North-Holland, 1978."},{"issue":"1","key":"9062_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. A machine-oriented logic based on the resolution principle. J. ACM, 1965, 12(1): 23~41.","journal-title":"J. ACM"},{"key":"9062_CR19","unstructured":"Sutcliffe G, Suttner C. The TPTP problem library for automated theorem proving. http:\/\/www.cs.miami.edu\/~tptp\/ ."},{"key":"9062_CR20","unstructured":"The CADE ATP System Competition held at the Third International Joint Conference on Automated Reasoning, Seattle, USA, 2006. http:\/\/www.cs.miami.edu\/~tptp\/CASC\/J3\/"},{"issue":"2","key":"9062_CR21","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1006\/inco.1999.2863","volume":"162","author":"H Schutz","year":"2000","unstructured":"Schutz H, Geisler T. Efficient model generation through compilation. Information and Computation, 2000, 162(2): 138~157.","journal-title":"Information and Computation"},{"key":"9062_CR22","unstructured":"Morales J, Carro M, Hermenegildo M. Improving the compilation of Prolog to C using type and determinism information: Preliminary results. In Proc. Colloquium on Implementation of Constraint and Logic Programming Systems (ICLP Associated Workshop), Mumbai, India, December 2003, pp.89~102."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-007-9062-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-007-9062-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-007-9062-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T14:32:39Z","timestamp":1559399559000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-007-9062-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7]]},"references-count":22,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2007,7]]}},"alternative-id":["9062"],"URL":"https:\/\/doi.org\/10.1007\/s11390-007-9062-2","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,7]]}}}