{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:29:17Z","timestamp":1725568157153},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540405597"},{"type":"electronic","value":"9783540450856"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45085-6_16","type":"book-chapter","created":{"date-parts":[[2010,10,26]],"date-time":"2010-10-26T13:13:30Z","timestamp":1288098810000},"page":"197-211","source":"Crossref","is-referenced-by-count":6,"title":["Canonization for Disjoint Unions of Theories"],"prefix":"10.1007","author":[{"given":"Sava","family":"Krsti\u0107","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sylvain","family":"Conchon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term Rewriting and All That","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, United Kingdom (1998)"},{"key":"16_CR2","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1006\/inco.2001.3118","volume":"178","author":"F. Baader","year":"2002","unstructured":"Baader, F., Tinelli, C.: Deciding the word problem in the union of equational theories. Information and Computation\u00a0178, 346\u2013390 (2002)","journal-title":"Information and Computation"},{"key":"16_CR3","unstructured":"Barrett, C.: Checking Validity of Quantifier-free formulas in Combinations of First- Order Theories. PhD thesis, Stanford University (2002)"},{"key":"16_CR4","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. Barrett","year":"1996","unstructured":"Barrett, C., 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)"},{"key":"16_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/3-540-45988-X_11","volume-title":"Frontiers of Combining Systems","author":"C.W. Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: A generalization of Shostak\u2019s method for combining decision procedures. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol.\u00a02309, pp. 132\u2013147. Springer, Heidelberg (2002)"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/3-540-61474-5_92","volume-title":"Computer Aided Verification","author":"N. Bj\u00f8rner","year":"1996","unstructured":"Bj\u00f8rner, N., et al.: Deductive-algorithmic verification of reactive and real-time systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 415\u2013418. Springer, Heidelberg (1996)"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/3-540-36577-X_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Conchon","year":"2003","unstructured":"Conchon, S., Krsti\u0107, S.: Strategies for combining decision procedures. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 537\u2013552. Springer, Heidelberg (2003)"},{"key":"16_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/3-540-61511-3_107","volume-title":"Automated Deduction - Cade-13","author":"D. Cyrluk","year":"1996","unstructured":"Cyrluk, D., Lincoln, P., Shankar, N.: On Shostak\u2019s decision procedure for combinations of theories. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 463\u2013477. Springer, Heidelberg (1996)"},{"key":"16_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1007\/3-540-45620-1_28","volume-title":"Automated Deduction - CADE-18","author":"H. Ganzinger","year":"2002","unstructured":"Ganzinger, H.: Shostak light. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 332\u2013347. Springer, Heidelberg (2002)"},{"key":"16_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-45988-X_8","volume-title":"Frontiers of Combining Systems","author":"D. Kapur","year":"2002","unstructured":"Kapur, D.: A rewrite rule based framework for combining decision procedures. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol.\u00a02309, pp. 87\u2013103. Springer, Heidelberg (2002)"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Krsti\u0107, S., Conchon, S.: Canonization for disjoint union of theories. Technical Report CSE-03-003, OHSU (2003)","DOI":"10.1007\/978-3-540-45085-6_16"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-540-40007-3_24","volume-title":"Formal Methods at the Crossroads. From Panacea to Foundational Support","author":"Z. Manna","year":"2003","unstructured":"Manna, Z., Zarba, C.G.: Combining decision procedures. In: Aichernig, B.K., Maibaum, T. (eds.) Formal Methods at the Crossroads. From Panacea to Foundational Support. LNCS, vol.\u00a02757, pp. 381\u2013422. Springer, Heidelberg (2003)"},{"issue":"2","key":"16_CR13","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"16_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal verification for faulttolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering\u00a021(2), 107\u2013125 (1995)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"16_CR15","doi-asserted-by":"crossref","first-page":"15","DOI":"10.4064\/cm-30-1-15-25","volume":"30","author":"D. Pigozzi","year":"1974","unstructured":"Pigozzi, D.: The join of equational thories. Colloquium Mathematicum\u00a030, 15\u201325 (1974)","journal-title":"Colloquium Mathematicum"},{"key":"16_CR16","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1109\/LICS.2001.932479","volume-title":"Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS-2001)","author":"H. Rue\u00df","year":"2001","unstructured":"Rue\u00df, H., Shankar, N.: Deconstructing Shostak. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS-2001), pp. 19\u201328. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45614-7_1","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"N. Shankar","year":"2002","unstructured":"Shankar, N.: Little engines of proof. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 1\u201320. Springer, Heidelberg (2002)"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45610-4_1","volume-title":"Rewriting Techniques and Applications","author":"N. Shankar","year":"2002","unstructured":"Shankar, N., Rue\u00df, H.: Combining Shostak theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, pp. 1\u201319. Springer, Heidelberg (2002)"},{"issue":"1","key":"16_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. Journal of the ACM\u00a031(1), 1\u201312 (1984)","journal-title":"Journal of the ACM"},{"key":"16_CR20","series-title":"Applied Logic","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-94-009-0349-4_5","volume-title":"Frontiers of Combining Systems: Proceedings of the 1st International Workshop","author":"C. Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson\u2013Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems: Proceedings of the 1st International Workshop, Munich, Germany. Applied Logic, pp. 103\u2013120. Kluwer, Dordrecht (1996)"},{"key":"16_CR21","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/S0304-3975(01)00332-2","volume":"290","author":"C. Tinelli","year":"2003","unstructured":"Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theoretical Computer Science\u00a0290, 291\u2013353 (2003)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-19"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45085-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,12]],"date-time":"2021-11-12T18:07:13Z","timestamp":1636740433000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45085-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540405597","9783540450856"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45085-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}