{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:44:35Z","timestamp":1725576275293},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540232124"},{"type":"electronic","value":"9783540302100"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30210-0_9","type":"book-chapter","created":{"date-parts":[[2011,1,18]],"date-time":"2011-01-18T10:34:36Z","timestamp":1295346876000},"page":"94-102","source":"Crossref","is-referenced-by-count":3,"title":["Extending Finite Model Searching with Congruence Closure Computation"],"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","reference":[{"issue":"4","key":"9_CR1","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"P.J. Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM\u00a027(4), 758\u2013771 (1980)","journal-title":"J. ACM"},{"key":"9_CR2","unstructured":"Fujita, M., Slaney, J., Bennett, F.: Automatic generation of some results in finite algebra. In: Proc. 13th IJCAI, pp. 52\u201357 (1993)"},{"key":"9_CR3","series-title":"LNAI","first-page":"776","volume-title":"Automated Deduction - CADE-11","author":"R. Hasegawa","year":"1992","unstructured":"Hasegawa, R., Koshimura, M., Fujita, H.: MGTP: A parallel theorem prover based on lazy model generation. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 776\u2013780. Springer, Heidelberg (1992)"},{"key":"9_CR4","unstructured":"Kim, S., Zhang, H.: ModGen: Theorem proving by model generation. In: Proc. 12th AAAI, pp. 162\u2013167 (1994)"},{"issue":"1","key":"9_CR5","first-page":"32","volume":"13","author":"V. Kumar","year":"1992","unstructured":"Kumar, V.: Algorithms for constraint satisfaction problems: A survey. AI Magazine\u00a013(1), 32\u201344 (1992)","journal-title":"AI Magazine"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"9th International Conference on Automated Deduction","author":"R. Manthey","year":"1988","unstructured":"Manthey, R., Bry, F.: SATCHMO: A theorem prover implemented in Prolog. In: Lusk, E.\u2018., Overbeek, R. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 415\u2013434. Springer, Heidelberg (1988)"},{"key":"9_CR7","unstructured":"McCune, W.: A Davis-Putnam program and its application to finite first-order model search: Quasigroup existence problems. Technical Report ANL\/MCS-TM-194, Argonne National Laboratory (1994)"},{"issue":"2","key":"9_CR8","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"J. ACM"},{"key":"9_CR9","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-39813-4_5","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Nieuwenhuis","year":"2003","unstructured":"Nieuwenhuis, R., Oliveras, A.: Congruence closure with integer offsets. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS (LNAI), vol.\u00a02850, pp. 78\u201390. Springer, Heidelberg (2003)"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"798","DOI":"10.1007\/3-540-58156-1_63","volume-title":"Automated Deduction - CADE-12","author":"J. Slaney","year":"1994","unstructured":"Slaney, J.: FINDER: Finite domain enumerator \u2013 system description. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 798\u2013801. Springer, Heidelberg (1994)"},{"issue":"2","key":"9_CR11","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0898-1221(94)00219-B","volume":"29","author":"J. Slaney","year":"1995","unstructured":"Slaney, J., Fujita, M., Stickel, M.: Automated reasoning and exhaustive search: Quasigroup existence problems. Computers and Mathematics with Applications\u00a029(2), 115\u2013132 (1995)","journal-title":"Computers and Mathematics with Applications"},{"key":"9_CR12","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP problem library for automated theorem proving, \n                    \n                      http:\/\/www.cs.miami.edu\/~tptp\/"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"753","DOI":"10.1007\/3-540-58156-1_54","volume-title":"Automated Deduction - CADE-12","author":"J. Zhang","year":"1994","unstructured":"Zhang, J.: Problems on the generation of finite models. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 753\u2013757. Springer, Heidelberg (1994)"},{"issue":"1","key":"9_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00244457","volume":"17","author":"J. Zhang","year":"1996","unstructured":"Zhang, J.: Constructing finite algebras with FALCON. J. Automated Reasoning\u00a017(1), 1\u201322 (1996)","journal-title":"J. Automated Reasoning"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/3-540-60299-2_24","volume-title":"Principles and Practice of Constraint Programming - CP \u201995","author":"J. Zhang","year":"1995","unstructured":"Zhang, J., Zhang, H.: Constraint propagation in model generation. In: Montanari, U., Rossi, F. (eds.) CP 1995. LNCS, vol.\u00a0976, pp. 398\u2013414. Springer, Heidelberg (1995)"},{"key":"9_CR16","unstructured":"Zhang, J., Zhang, H.: SEM: A system for enumerating models. In: Proc. 14th IJCAI, pp. 298\u2013303 (1995)"}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30210-0_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:56:01Z","timestamp":1620014161000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30210-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540232124","9783540302100"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30210-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}