{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T01:07:39Z","timestamp":1768266459377,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540255963","type":"print"},{"value":"9783540320333","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32033-3_33","type":"book-chapter","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T00:20:02Z","timestamp":1285633202000},"page":"453-468","source":"Crossref","is-referenced-by-count":50,"title":["Proof-Producing Congruence Closure"],"prefix":"10.1007","author":[{"given":"Robert","family":"Nieuwenhuis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Albert","family":"Oliveras","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"33_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/3-540-45620-1_17","volume-title":"Automated Deduction - CADE-18","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 195\u2013210. Springer, Heidelberg (2002)"},{"key":"33_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-45657-0_18","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2002","unstructured":"Barrett, C., Dill, D., Stump, A.: Checking satisfiability of first-order formulas by incremental translation into sat. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 236. Springer, Heidelberg (2002)"},{"key":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/10721959_5","volume-title":"Automated Deduction - CADE-17","author":"L. Bachmair","year":"2000","unstructured":"Bachmair, L., Tiwari, A.: Abstract congruence closure and specializations. In: McAllester, D. (ed.) CADE 2000. LNCS, vol.\u00a01831, pp. 64\u201378. Springer, Heidelberg (2000)"},{"key":"33_CR4","volume-title":"Introduction to algorithms","author":"T.T. Cormen","year":"1990","unstructured":"Cormen, T.T., Leiserson, C.E., Rivest, R.L.: Introduction to algorithms. MIT Press, Cambridge (1990)"},{"issue":"7","key":"33_CR5","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Comm. of the ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Comm. of the ACM"},{"key":"33_CR6","unstructured":"de Moura, L., Rue\u00df, H.: Lemmas on demand for satisfiability solvers. In: Procs. 5th Int. Symp. on the Theory and Applications of Satisfiability Testing, SAT 2002, pp. 244\u2013251 (2002)"},{"key":"33_CR7","unstructured":"de Moura, L., Rue\u00df, H., Shankar, N.: Justifying equality. In: Proc. of the Second Workshop on Pragmatics of Decision Procedures in Automated Reasoning, Cork, Ireland (2004)"},{"key":"33_CR8","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"issue":"4","key":"33_CR9","doi-asserted-by":"crossref","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 subexpressions problem. J. of the Association for Computing Machinery\u00a027(4), 758\u2013771 (1980)","journal-title":"J. of the Association for Computing Machinery"},{"key":"33_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Computer Aided Verification","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem proving using lazy proof explanation. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 355\u2013367. Springer, Heidelberg (2003)"},{"key":"33_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"33_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Rewriting Techniques and Applications","author":"D. Kapur","year":"1997","unstructured":"Kapur, D.: Shostak\u2019s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol.\u00a01232, Springer, Heidelberg (1997)"},{"key":"33_CR13","unstructured":"Klapper, R., Stump, A.: Validated proof-producing decision procedures. In: Proceedings of the Second Workshop on Pragmatics of Decision Procedures in Automated Reasoning, Cork, Ireland (2004)"},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. 38th Design Automation Conference, DAC 2001 (2001)","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"33_CR15","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures bases on congruence closure. Journal of the Association for Computing Machinery\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"33_CR16","series-title":"Lecture Notes in Computer Science","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, vol.\u00a02850, pp. 78\u201390. Springer, Heidelberg (2003)"},{"key":"33_CR17","unstructured":"Stump, A., Dill, D.L.: Generating proofs from a decision procedure. In: Pnueli, A., Traverso, P. (eds.) Proceedings of the FLoC Workshop on Run-Time Result Verification, Trento, Italy (1999)"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"Shostak, R.E.: An algorithm for reasoning about equality. Commun. ACM\u00a021(7) (1978)","DOI":"10.1145\/359545.359570"},{"issue":"2","key":"33_CR19","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/321879.321884","volume":"22","author":"R.E. Tarjan","year":"1975","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. Journal of the ACM (JACM)\u00a022(2), 215\u2013225 (1975)","journal-title":"Journal of the ACM (JACM)"},{"issue":"2","key":"33_CR20","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/0022-0000(79)90042-4","volume":"18","author":"R.E. Tarjan","year":"1979","unstructured":"Tarjan, R.E.: A class of algorithms that require nonlinear time to maintain disjoint sets. J. Comput. and Sys. Sci.\u00a018(2), 110\u2013127 (1979)","journal-title":"J. Comput. and Sys. Sci."},{"key":"33_CR21","unstructured":"Tiwari, A., Vigneron, L.: Implementation of Abstract Congruence Closure with randomly generated CC problem instances (2001), At \n                  \n                    http:\/\/www.csl.sri.com\/users\/tiwari"}],"container-title":["Lecture Notes in Computer Science","Term Rewriting and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32033-3_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:45:35Z","timestamp":1620013535000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}