{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:27:42Z","timestamp":1767929262468,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":61,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540205272","type":"print"},{"value":"9783540400073","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-40007-3_24","type":"book-chapter","created":{"date-parts":[[2010,6,25]],"date-time":"2010-06-25T20:04:10Z","timestamp":1277496250000},"page":"381-422","source":"Crossref","is-referenced-by-count":26,"title":["Combining Decision Procedures"],"prefix":"10.1007","author":[{"given":"Zohar","family":"Manna","sequence":"first","affiliation":[]},{"given":"Calogero G.","family":"Zarba","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland Publishing Company, Amsterdam (1954)"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/3-540-45406-3_3","volume-title":"Constraints in Computational Logics. Theory and Applications","author":"F. Baader","year":"2001","unstructured":"Baader, F., Schulz, K.U.: Combining constraint solving. In: Comon, H., March\u00e9, C., Treinen, R. (eds.) CCL 1999. LNCS, vol.\u00a02002, pp. 104\u2013158. Springer, Heidelberg (2001)"},{"key":"24_CR3","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.L., Levitt, J.L.: 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":"24_CR4","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\u2013146. Springer, Heidelberg (2002)"},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"411","DOI":"10.2307\/2300300","volume":"41","author":"E.T. Bell","year":"1934","unstructured":"Bell, E.T.: Exponential numbers. American Mathematical Monthly\u00a041, 411\u2013419 (1934)","journal-title":"American Mathematical Monthly"},{"key":"24_CR6","unstructured":"Bj\u00f8rner, N.S.: Integrating Decision Procedures for Temporal Verification. PhD thesis, Stanford University (1998)"},{"issue":"3","key":"24_CR7","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1023\/A:1008700623084","volume":"16","author":"N.S. Bj\u00f8rner","year":"2000","unstructured":"Bj\u00f8rner, N.S., Browne, A., Col\u00f3n, M., Finkbeiner, B., Manna, Z., Sipma, H.B., Uribe, T.E.: Verifying temporal properties of reactive systems: A STeP tutorial. Formal Methods in System Design\u00a016(3), 227\u2013270 (2000)","journal-title":"Formal Methods in System Design"},{"key":"24_CR8","series-title":"Lecture Notes in Artificial Intelligence","first-page":"127","volume-title":"Automated Deduction in Classical and Non-Classical Logics","author":"D. Cantone","year":"2000","unstructured":"Cantone, D., Zarba, C.G.: A new fast tableau-based decision procedure for an unquantified fragment of set theory. In: Caferra, R., Salzer, G. (eds.) FTP 1998. LNCS (LNAI), vol.\u00a01761, pp. 127\u2013137. Springer, Heidelberg (2000)"},{"key":"24_CR9","doi-asserted-by":"publisher","first-page":"101","DOI":"10.2307\/2269030","volume":"1","author":"A. Church","year":"1936","unstructured":"Church, A.: A note on the Entscheidungsproblem. Journal of Symbolic Logic\u00a01, 101\u2013102 (1936)","journal-title":"Journal of Symbolic Logic"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"24_CR11","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol.\u00a07, pp. 91\u201399. Edinburgh University Press (1972)"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/3-540-54834-3_24","volume-title":"VDM \u201991","author":"D. Craigen","year":"1991","unstructured":"Craigen, D., Kromodimoeljo, S., Meisels, I., Pase, B., Saaltink, M.: EVES: An overview. In: Prehn, S., Toetenel, H. (eds.) VDM 1991. LNCS, vol.\u00a0552, pp. 389\u2013405. Springer, Heidelberg (1991)"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","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, vol.\u00a01104, pp. 463\u2013477. Springer, Heidelberg (1996)"},{"key":"24_CR14","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"J.H. Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. Journal of Symbolic Computation\u00a05, 29\u201335 (1988)","journal-title":"Journal of Symbolic Computation"},{"key":"24_CR15","volume-title":"Asymptotic Methods in Analysis","author":"N.G. Bruijn de","year":"1958","unstructured":"de Bruijn, N.G.: Asymptotic Methods in Analysis. North-Holland Publishing Company, Amsterdam (1958)"},{"key":"24_CR16","unstructured":"Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended static checking. Technical Report 159, Compaq System Research Center (1998)"},{"issue":"4","key":"24_CR17","doi-asserted-by":"crossref","first-page":"652","DOI":"10.1145\/322092.322104","volume":"25","author":"P. Downey","year":"1978","unstructured":"Downey, P., Sethi, R.: Assignment commands with array references. Journal of the Association for Computing Machinery\u00a025(4), 652\u2013666 (1978)","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"4","key":"24_CR18","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 subexpression problem. Journal of the Association for Computing Machinery\u00a027(4), 758\u2013771 (1980)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"24_CR19","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"2000","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press, London (2000)","edition":"2"},{"issue":"1","key":"24_CR20","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1137\/0204006","volume":"4","author":"J. Ferrante","year":"1975","unstructured":"Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM Journal on Computing\u00a04(1), 69\u201376 (1975)","journal-title":"SIAM Journal on Computing"},{"key":"24_CR21","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.-C. Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J.-C., 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, pp. 246\u2013249. Springer, Heidelberg (2001)"},{"key":"24_CR22","unstructured":"Fischer, M.J., Rabin, M.O.: Super-exponential complexity of Presburger arithmetic. In: Karp, R.M. (ed.) Complexity of Computation. SIAM-AMS proceedings, vol.\u00a07, pp. 27\u201342. American Mathematical Society (1974)"},{"key":"24_CR23","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\u2013346. Springer, Heidelberg (2002)"},{"key":"24_CR24","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\u2013102. Springer, Heidelberg (2002)"},{"key":"24_CR25","first-page":"191","volume":"20","author":"L.G. Khachiyan","year":"1979","unstructured":"Khachiyan, L.G.: A polynomial algorithm in linear programming. Soviet Mathematics Doklady\u00a020, 191\u2013194 (1979)","journal-title":"Soviet Mathematics Doklady"},{"key":"24_CR26","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Complexity of finitely presented algebras. In: Proceedings of the ninth annual ACM symposium on Theory of computing, pp. 164\u2013177 (1977)","DOI":"10.1145\/800105.803406"},{"key":"24_CR27","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Elements of Mathematical Logic","author":"G. Kreisel","year":"1967","unstructured":"Kreisel, G., Krivine, J.L.: Elements of Mathematical Logic. Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, Amsterdam (1967)"},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"Krsti\u0107, S., Conchon, S.: Canonization for disjoint union of theories. Technical Report CSE-03-003, Oregon Health and Science University (2003)","DOI":"10.1007\/978-3-540-45085-6_16"},{"issue":"3","key":"24_CR29","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/BF00245296","volume":"9","author":"J.-L. Lassez","year":"1992","unstructured":"Lassez, J.-L., Mahler, M.J.: On Fourier\u2019s algorithm for linear constraints. Journal of Automated Reasoning\u00a09(3), 373\u2013379 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR30","unstructured":"Levitt, J.L.: Formal Verification Techniques for Digital Systems. PhD thesis, Stanford University (1998)"},{"key":"24_CR31","first-page":"337","volume-title":"Theorem Prover in Circuit Design: Theory, Practice and Experience","author":"B. Levy","year":"1992","unstructured":"Levy, B., Filippenko, I., Marcus, L., Menas, T.: Using the state delta verification system (SDVS) for hardware verification. In: Melham, T.F., Stavridou, V., Boute, R.T. (eds.) Theorem Prover in Circuit Design: Theory, Practice and Experience, pp. 337\u2013360. Elsevier Science, Amsterdam (1992)"},{"key":"24_CR32","doi-asserted-by":"crossref","unstructured":"Luckham, D.C., German, S.M., von Henke, F.W., Karp, R.A., Milne, P.W., Oppen, D.C., Polak, W., Scherlis, W.L.: Stanford pascal verifier user manual. Technical Report STAN-CS-79-731, Stanford University (1979)","DOI":"10.21236\/ADA071900"},{"key":"24_CR33","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0049-237X(08)70846-2","volume-title":"Second Scandinavian Logic Symposium","author":"Y.V. Matiyasevich","year":"1971","unstructured":"Matiyasevich, Y.V.: Diophantine representation of recursively enumerable predicates. In: Fenstad, J.E. (ed.) Second Scandinavian Logic Symposium. Studies in Logic and the Foundations of Mathematics, vol.\u00a063, pp. 171\u2013177. North-Holland Publishing Company, Amsterdam (1971)"},{"key":"24_CR34","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress 62 (1962)"},{"key":"24_CR35","unstructured":"Nelson, G.: Techniques for program verification. Technical Report CSL-81-10, Xerox Palo Alto Research Center (1981)"},{"key":"24_CR36","doi-asserted-by":"crossref","unstructured":"Nelson, G.: Combining satisfiability procedures by equality sharing. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automated Theorem Proving: After 25 Years. Contemporary Mathematics, vol.\u00a029, pp. 201\u2013211. American Mathematical Society (1984)","DOI":"10.1090\/conm\/029\/11"},{"issue":"2","key":"24_CR37","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":"24_CR38","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 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"},{"issue":"3","key":"24_CR39","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1016\/0022-0000(78)90021-1","volume":"16","author":"D.C. Oppen","year":"1978","unstructured":"Oppen, D.C.: A $2^{2^{2^{pn}}}$ upper bound on the complexity of Presburger arithmetic. Journal of Computer and System Sciences\u00a016(3), 323\u2013332 (1978)","journal-title":"Journal of Computer and System Sciences"},{"key":"24_CR40","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"D.C. Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, convexity and combinations of theories. Theoretical Computer Science\u00a012, 291\u2013302 (1980)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"24_CR41","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1145\/322203.322204","volume":"27","author":"D.C. Oppen","year":"1980","unstructured":"Oppen, D.C.: Reasoning about recursively defined data structures. Journal of the Association for Computing Machinery\u00a027(3), 403\u2013411 (1980)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"24_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.K.: PVS: Combining specification, proof checking and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 411\u2013414. Springer, Heidelberg (1996)"},{"issue":"4","key":"24_CR43","doi-asserted-by":"crossref","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"C.H. Papadimitriou","year":"1981","unstructured":"Papadimitriou, C.H.: On the complexity of integer programming. Journal of the Association for Computing Machinery\u00a028(4), 765\u2013768 (1981)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"24_CR44","unstructured":"Presburger, M.: \u00dcber die vollst\u00e4ndigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen die addition als einzige operation hervortritt. In: Comptes Rendus du Premier Congr\u00e8s des Math\u00e9maticienes des Pays Slaves, pp. 92\u2013101 (1929)"},{"key":"24_CR45","series-title":"Applied Logic Series","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/978-94-009-0349-4_6","volume-title":"Frontiers of Combining Systems","author":"C. Ringeissen","year":"1996","unstructured":"Ringeissen, C.: Cooperation of decision procedures for the satisfiability problem. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems. Applied Logic Series, vol.\u00a03, pp. 121\u2013140. Kluwer Academic Publishers, Dordrecht (1996)"},{"key":"24_CR46","first-page":"19","volume-title":"Sixteenth Annual IEEE Symposium on Logic in Computer Science","author":"H. Rue\u00df","year":"2001","unstructured":"Rue\u00df, H., Shankar, N.: Deconstructing Shostak. In: Sixteenth Annual IEEE Symposium on Logic in Computer Science, pp. 19\u201328. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"24_CR47","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\u201318. Springer, Heidelberg (2002)"},{"issue":"7","key":"24_CR48","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"R.E. Shostak","year":"1978","unstructured":"Shostak, R.E.: An algorithm for reasoning about equality. Communications of the Association for Computing Machinery\u00a021(7), 583\u2013585 (1978)","journal-title":"Communications of the Association for Computing Machinery"},{"issue":"2","key":"24_CR49","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R.E. Shostak","year":"1979","unstructured":"Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. Journal of the Association for Computing Machinery\u00a026(2), 351\u2013360 (1979)","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"1","key":"24_CR50","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combination of theories. Journal of the Association for Computing Machinery\u00a031(1), 1\u201312 (1984)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"24_CR51","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., Barret, C.W., Dill, D.L.: CVC: A cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 500\u2013504. Springer, Heidelberg (2002)"},{"key":"24_CR52","first-page":"29","volume-title":"Sixteenth Annual IEEE Symposium on Logic in Computer Science","author":"A. Stump","year":"2001","unstructured":"Stump, A., Barret, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Sixteenth Annual IEEE Symposium on Logic in Computer Science, pp. 29\u201337. IEEE Computer Society Press, Los Alamitos (2001)"},{"issue":"1","key":"24_CR53","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1145\/322169.322185","volume":"27","author":"N. Suzuki","year":"1980","unstructured":"Suzuki, N., Jefferson, D.: Verification decidability of Presburger array programs. Journal of the Association for Computing Machinery\u00a027(1), 191\u2013205 (1980)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"24_CR54","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press (1951)","DOI":"10.1525\/9780520348097"},{"key":"24_CR55","unstructured":"Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. Technical Report 02-03, Department of Computer Science, University of Iowa (2002)"},{"key":"24_CR56","series-title":"Applied Logic Series","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-94-009-0349-4_5","volume-title":"Frontiers of Combining Systems","author":"C. Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems. Applied Logic Series, vol.\u00a03, pp. 103\u2013120. Kluwer Academic Publishers, Dordrecht (1996)"},{"issue":"1","key":"24_CR57","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(1), 291\u2013353 (2003)","journal-title":"Theoretical Computer Science"},{"key":"24_CR58","unstructured":"Tiwari, A.: Decision Procedures in Automated Deduction. PhD thesis, State University of New York at Stony Brook (2000)"},{"key":"24_CR59","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1112\/plms\/s2-42.1.230","volume":"42","author":"A.M. Turing","year":"1936","unstructured":"Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society\u00a042, 230\u2013265 (1936)","journal-title":"Proceedings of the London Mathematical Society"},{"key":"24_CR60","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-45620-1_30","volume-title":"Automated Deduction - CADE-18","author":"C.G. Zarba","year":"2002","unstructured":"Zarba, C.G.: Combining multisets with integers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 363\u2013376. Springer, Heidelberg (2002)"},{"key":"24_CR61","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/3-540-45616-3_22","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"C.G. Zarba","year":"2002","unstructured":"Zarba, C.G.: A tableau calculus for combining non-disjoint theories. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 315\u2013329. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods at the Crossroads. From Panacea to Foundational Support"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-40007-3_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,30]],"date-time":"2021-10-30T05:31:37Z","timestamp":1635571897000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-40007-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540205272","9783540400073"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-40007-3_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}