{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:04:26Z","timestamp":1725663866548},"publisher-location":"Berlin, Heidelberg","reference-count":15,"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_54","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:23:41Z","timestamp":1330269821000},"page":"753-757","source":"Crossref","is-referenced-by-count":7,"title":["Problems on the generation of finite models"],"prefix":"10.1007","author":[{"given":"Jian","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"54_CR1","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1080\/00029890.1993.11990393","volume":"100","author":"S. Burris","year":"1993","unstructured":"Burris, S., and Lee, S., \u201cTarski's high school identities,\u201d The Amer. Math. Monthly 100 (1993) 231\u2013236.","journal-title":"The Amer. Math. Monthly"},{"key":"54_CR2","unstructured":"Fujita, M. et al, \u201cAutomatic generation of some results in finite algebra,\u201d Proc. 13th IJCAI (1993) 52\u201357."},{"key":"54_CR3","first-page":"776","volume":"607","author":"R. Hasegawa","year":"1992","unstructured":"Hasegawa, R. et al, \u201c'MGTP: A parallel theorem prover based on lazy model generation,\u201d Proc. 11th CADE, LNAI 607 (1992) 776\u2013780.","journal-title":"Proc. 11th CADE, LNAI"},{"key":"54_CR4","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0097-3165(90)90015-O","volume":"A54","author":"G. Kolesova","year":"1990","unstructured":"Kolesova, G. et al, \u201cOn the number of 8\u00d78 Latin squares,\u201d J. Combinatorial Theory A54 (1990) 143\u2013148.","journal-title":"J. Combinatorial Theory"},{"key":"54_CR5","first-page":"415","volume":"310","author":"R. Manthey","year":"1988","unstructured":"Manthey, R., and Bry, F.,\u201cSATCHMO: A theorem prover implemented in Prolog,\u201d Proc. 9th CADE, LNCS 310 (1988) 415\u2013434.","journal-title":"Proc. 9th CADE, LNCS"},{"key":"54_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00881862","volume":"10","author":"W. McCune","year":"1993","unstructured":"McCune, W., \u201cSingle axioms for groups and Abelian groups with various operations,\u201d J. Automated Reasoning 10 (1993) 1\u201313.","journal-title":"J. Automated Reasoning"},{"key":"54_CR7","unstructured":"Peterson, J. G., \u201cThe possible shortest single axioms for EC-tautologies,\u201d Report No. 105, Dept. of Mathematics, Univ. of Auckland (1977)."},{"key":"54_CR8","unstructured":"Slaney, J., \u201cFINDER: Finite domain enumerator. Version 3.0 notes and guide,\u201d Australian National University, (1993)."},{"key":"54_CR9","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/322307.322308","volume":"29","author":"S. Winker","year":"1982","unstructured":"Winker, S., \u201cGeneration and verification of finite models and counterexamples using an automated theorem prover answering two open questions,\u201d J. ACM 29 (1982) 273\u2013284.","journal-title":"J. ACM"},{"key":"54_CR10","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/BF00244359","volume":"6","author":"S. Winker","year":"1990","unstructured":"Winker, S., \u201cRobbins algebra: Conditions that make a near-Boolean algebra Boolean,\u201d J. Automated Reasoning 6 (1990) 465\u2013489.","journal-title":"J. Automated Reasoning"},{"key":"54_CR11","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/0004-3702(84)90054-7","volume":"22","author":"L. Wos","year":"1984","unstructured":"Wos, L. et al, \u201cA new use of an automated reasoning assistant: Open questions in equivalential calculus and the study of infinite domains,\u201d Artificial Intelligence 22 (1984) 303\u2013356.","journal-title":"Artificial Intelligence"},{"key":"54_CR12","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF00245821","volume":"6","author":"L. Wos","year":"1990","unstructured":"Wos, L. \u201cMeeting the challenge of fifty years of logic,\u201d J. Automated Reasoning 6 (1990) 213\u2013232.","journal-title":"J. Automated Reasoning"},{"key":"54_CR13","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00881795","volume":"10","author":"L. Wos","year":"1993","unstructured":"Wos, L., \u201cThe kernel strategy and its use for the study of combinatory logic,\u201d J. Automated Reasoning 10 (1993) 287\u2013343.","journal-title":"J. Automated Reasoning"},{"key":"54_CR14","unstructured":"Zhang, H., and Stickel, M., \u201cImplementing the Davis-Putnam method by tries,\u201d submitted to AAAI-94."},{"key":"54_CR15","unstructured":"Zhang, J., \u201cSearch for models of equational theories,\u201d Proc. 3rd Int'l Conf. for Young Computer Scientists (ICYCS-93), Beijing (1993) 2.60\u201363."}],"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_54.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:11:58Z","timestamp":1619572318000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_54","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}