{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:44:21Z","timestamp":1725576261371},"publisher-location":"Berlin, Heidelberg","reference-count":12,"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_7","type":"book-chapter","created":{"date-parts":[[2011,1,18]],"date-time":"2011-01-18T10:34:36Z","timestamp":1295346876000},"page":"66-79","source":"Crossref","is-referenced-by-count":2,"title":["A Decision Procedure for Equality Logic with Uninterpreted Functions"],"prefix":"10.1007","author":[{"given":"Olga","family":"Tveretina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Solvable cases of the decision problem","author":"W. Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable cases of the decision problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1954)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods in Computer-Aided Design","author":"C.W. Barrett","year":"1996","unstructured":"Barrett, C.W., Dill, D., Levitt, J.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 187\u2013201. Springer, Heidelberg (1996)"},{"issue":"4","key":"7_CR3","doi-asserted-by":"publisher","first-page":"604","DOI":"10.1145\/566385.566390","volume":"3","author":"R. Bryant","year":"2002","unstructured":"Bryant, R., Velev, M.: Boolean satisfiability with transitivity constraints. ACM Transactions on Computational Logic\u00a03(4), 604\u2013627 (2002)","journal-title":"ACM Transactions on Computational Logic"},{"key":"7_CR4","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. Burch","year":"1994","unstructured":"Burch, J., Dill, D.: Automated verification of pipelined microprocesoor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"key":"7_CR5","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"7","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the Association for Computing Machinery\u00a07, 394\u2013397 (1962)","journal-title":"Communications of the Association for Computing Machinery"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/BFb0028749","volume-title":"Computer Aided Verification","author":"A. Goel","year":"1998","unstructured":"Goel, A., Sajid, K., Zhou, H., Aziz, A., Singhal, V.: BDD based procedures for a theory of equality with uninterpreted functions. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 244\u2013255. Springer, Heidelberg (1998)"},{"key":"7_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/3-540-44404-1_11","volume-title":"Logic for Programming and Automated Reasoning","author":"J. Groote","year":"2000","unstructured":"Groote, J., van de Pol, J.: Equational binary decision diagrams. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 161\u2013178. Springer, Heidelberg (2000)"},{"key":"7_CR8","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":"7_CR9","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":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/3-540-44585-4_13","volume-title":"Computer Aided Verification","author":"Y. Rodeh","year":"2001","unstructured":"Rodeh, Y., Shtrichman, O.: Finite instantiations in equivalence logic with uninterpreted functions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 144\u2013154. Springer, Heidelberg (2001)"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Shostak, R.: An algorithm for reasoning about equality. Communications of the ACM 21 (1978)","DOI":"10.1145\/359545.359570"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus, Consultant Bureau, New York-London. Studies in Constructive Mathematics and Mathematical Logic, Part 2, pp. 115\u2013125 (1968)","DOI":"10.1007\/978-1-4899-5327-8_25"}],"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_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:49:28Z","timestamp":1605761368000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30210-0_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540232124","9783540302100"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30210-0_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}