{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:10:42Z","timestamp":1725664242785},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602996"},{"type":"electronic","value":"9783540447887"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60299-2_24","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:14:42Z","timestamp":1330280082000},"page":"398-414","source":"Crossref","is-referenced-by-count":3,"title":["Constraint propagation in model generation"],"prefix":"10.1007","author":[{"given":"Jian","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hantao","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1016\/0004-3702(88)90023-9","volume":"35","author":"W. Bibel","year":"1988","unstructured":"Bibel, W., \u201cConstraint satisfaction from a deductive viewpoint,\u201d Artificial Intelligence 35 (1988) 401\u2013413.","journal-title":"Artificial Intelligence"},{"key":"24_CR2","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/3-540-58156-1_6","volume":"814","author":"C. Bourely","year":"1994","unstructured":"Bourely, C., Caferra, R., and Peltier, N., \u201cA method for building models automatically: Experiments with an extension of OTTER,\u201d Proc. 12th Conf. on Automated Deduction (CADE-12), Springer LNAI 814 (1994) 72\u201386.","journal-title":"Proc. 12th Conf. on Automated Deduction (CADE-12), Springer LNAI"},{"key":"24_CR3","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., and Putnam, H., \u201cA computing procedure for quantification theory,\u201d J. ACM\n7 (1960) 201\u2013215.","journal-title":"J. ACM"},{"unstructured":"Fujita, M., Slaney, J., and Bennett, F., \u201cAutomatic generation of some results in finite algebra,\u201d Proc. 13th IJCAI (1993) 52\u201357.","key":"24_CR4"},{"key":"24_CR5","first-page":"776","volume":"607","author":"R. Hasegawa","year":"1992","unstructured":"Hasegawa, R., Koshimura, M., and Fujita, H., \u201cMGTP: A parallel theorem prover based on lazy model generation,\u201d Proc. 11th Conf. on Automated Deduction (CADE-11) Springer LNAI 607 (1992) 776\u2013780.","journal-title":"Proc. 11th Conf. on Automated Deduction (CADE-11) Springer LNAI"},{"key":"24_CR6","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"19\/20","author":"J. Jaffar","year":"1994","unstructured":"Jaffar, J., and Maher, M.J., \u201cConstraint logic programming: A survey,\u201d J. of Logic Programming 19\/20 (1994) 503\u2013581.","journal-title":"J. of Logic Programming"},{"unstructured":"Kim, S., and Zhang, H., \u201cModGen: Theorem proving by model generation,\u201d Proc. AAAI-94, Seattle (1994) 162\u2013167.","key":"24_CR7"},{"key":"24_CR8","first-page":"32","volume":"13","author":"V. Kumar","year":"1992","unstructured":"Kumar, V., \u201cAlgorithms for constraint satisfaction problems: A survey,\u201d AI Magazine 13 (1992) 32\u201344.","journal-title":"AI Magazine"},{"key":"24_CR9","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/0004-3702(94)90082-5","volume":"69","author":"S.-J. Lee","year":"1994","unstructured":"Lee, S.-J., and Plaisted, D. A., \u201cProblem solving by searching for models with a theorem prover,\u201d Artificial Intelligence 69 (1994) 205\u2013233.","journal-title":"Artificial Intelligence"},{"key":"24_CR10","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0004-3702(92)90003-G","volume":"58","author":"A.K. Mackworth","year":"1992","unstructured":"Mackworth, A.K., \u201cThe logic of constraint satisfaction,\u201d Artificial Intelligence 58 (1992) 3\u201320.","journal-title":"Artificial Intelligence"},{"key":"24_CR11","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 Conf. on Automated Deduction (CADE-9), LNCS 310 (1988) 415\u2013434.","journal-title":"Proc. 9th Conf. on Automated Deduction (CADE-9), LNCS"},{"key":"24_CR12","doi-asserted-by":"publisher","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. of Automated Reasoning 10 (1993) 1\u201313.","journal-title":"J. of Automated Reasoning"},{"unstructured":"McCune, W., \u201cA Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems,\u201d Technical Report ANL\/MCS-TM-194, Argonne National Laboratory (1994).","key":"24_CR13"},{"unstructured":"Slaney, J., \u201cFINDER: Finite domain enumerator. Version 3.0 notes and guide,\u201d Australian National University (1993).","key":"24_CR14"},{"doi-asserted-by":"crossref","unstructured":"Slaney, J., Stickel, M., and Fujita, M., \u201cAutomated reasoning and exhaustive search: Quasigroup existence problems,\u201d Computers and Mathematics with Applications 29 (1995).","key":"24_CR15","DOI":"10.1016\/0898-1221(94)00219-B"},{"key":"24_CR16","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BFb0019355","volume":"502","author":"T. Tammet","year":"1991","unstructured":"Tammet, T., \u2018Using resolution for deciding solvable classes and building finite models,\u2019 Baltic Computer Science: Selected Papers, Springer LNCS 502 (1991) 33\u201364.","journal-title":"Baltic Computer Science: Selected Papers, Springer LNCS"},{"key":"24_CR17","volume-title":"Automated Reasoning: 33 Basic Research Problems","author":"L. Wos","year":"1988","unstructured":"Wos, L., Automated Reasoning: 33 Basic Research Problems, Prentice-Hall, Englewood Cliffs, New Jersey (1988)."},{"doi-asserted-by":"crossref","unstructured":"Wos, L., and McCune, W., \u201cNegative paramodulation,\u201d Proc. 8th Conf. on Automated Deduction (CADE-8), Springer LNCS 230 (1986) J.H. Siekmann (ed.) 229\u2013239.","key":"24_CR18","DOI":"10.1007\/3-540-16780-3_93"},{"unstructured":"Zhang, H. and Stickel, M., \u201cImplementing the Davis-Putnam algorithm by tries,\u201d Technical Report, University of Iowa (1994).","key":"24_CR19"},{"doi-asserted-by":"crossref","unstructured":"Zhang, J., \u201cConstructing finite algebras with FALCON,\u201d J. of Automated Reasoning, to appear.","key":"24_CR20","DOI":"10.1007\/BF00247667"}],"container-title":["Lecture Notes in Computer Science","Principles and Practice of Constraint Programming \u2014 CP '95"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60299-2_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:36:54Z","timestamp":1619573814000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60299-2_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602996","9783540447887"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-60299-2_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}