{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:15:32Z","timestamp":1774988132750,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"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_34","type":"book-chapter","created":{"date-parts":[[2010,9,28]],"date-time":"2010-09-28T00:20:02Z","timestamp":1285633202000},"page":"469-483","source":"Crossref","is-referenced-by-count":7,"title":["The Algebra of Equality Proofs"],"prefix":"10.1007","author":[{"given":"Aaron","family":"Stump","sequence":"first","affiliation":[]},{"given":"Li-Yang","family":"Tan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"34_CR1","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 to SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 236. Springer, Heidelberg (2002)"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"key":"34_CR4","volume-title":"Introduction to Algorithms","author":"T. Cormen","year":"1992","unstructured":"Cormen, T., Leiserson, C., Rivest, R.: Introduction to Algorithms. MIT Press, Cambridge (1992)"},{"key":"34_CR5","unstructured":"de Moura, L., Rue\u00df, H., Shankar, N.: Justifying Equality. In: Ranise, S., Tinelli, C. (eds.) 2nd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (2004)"},{"key":"34_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer Aided Verification","author":"J. Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J., Owre, S., Rue\u00df, H., Shankar, N.: ICS: integrated canonizer and solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 246. Springer, Heidelberg (2001)"},{"key":"34_CR7","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D. Knuth","year":"1970","unstructured":"Knuth, D., Bendix, P.: SimpleWord Problems in Universal Algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, Oxford (1970)"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24730-2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Lahiri","year":"2004","unstructured":"Lahiri, S., Bryant, R., Goel, A., Talupur, M.: Revisiting Positive Equality. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 1\u201315. Springer, Heidelberg (2004)"},{"issue":"2","key":"34_CR9","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.: Fast decision procedures based 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":"34_CR10","unstructured":"Nieuwenhuis, R., Oliveras, A.: Union-Find and Congruence Closure Algorithms that Produce Proofs. In: Ranise, S., Tinelli, C. (eds.) 2nd International Workshop on Pragmatics of Decision Procedures in Automated Reasoning (2004) (short paper)"},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A.: Proof-producing Congruence Closure. In: Giesl, J. (ed.) 16th International Conference on Rewriting Techniques and Applications (2005) (under review)","DOI":"10.1007\/978-3-540-32033-3_33"},{"key":"34_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/3-540-48683-6_39","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"1999","unstructured":"Pnueli, A., Rodeh, Y., Shtrichman, O., Siegel, M.: Deciding Equality Formulas by Small Domains Instantiations. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 455\u2013469. Springer, Heidelberg (1999)"},{"key":"34_CR13","doi-asserted-by":"crossref","unstructured":"Ruess, H., Shankar, N.: Deconstructing Shostak. In: 16th IEEE Symposium on Logic in Computer Science (2001)","DOI":"10.1109\/LICS.2001.932479"},{"issue":"1","key":"34_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. Shostak","year":"1984","unstructured":"Shostak, R.: Deciding combinations of theories. Journal of the Association for Computing Machinery\u00a031(1), 1\u201312 (1984)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"34_CR15","unstructured":"Stump, A.: Checking Validities and Proofs with CVC and flea. PhD thesis, Stanford University (2002), available from \n                  \n                    http:\/\/www.cs.wustl.edu\/~stump\/"},{"key":"34_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45657-0_40","volume-title":"Computer Aided Verification","author":"A. Stump","year":"2002","unstructured":"Stump, A., Barrett, C., Dill, D.: CVC: a Cooperating Validity Checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 500. Springer, Heidelberg (2002)"},{"key":"34_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-48153-2_5","volume-title":"Correct Hardware Design and Verification Methods","author":"M. Velev","year":"1999","unstructured":"Velev, M., Bryant, R.: Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 37\u201353. Springer, Heidelberg (1999)"}],"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_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:45:36Z","timestamp":1620013536000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32033-3_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255963","9783540320333"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32033-3_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}