{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:06:18Z","timestamp":1767927978001,"version":"3.49.0"},"reference-count":29,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2005,4,1]],"date-time":"2005-04-01T00:00:00Z","timestamp":1112313600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2005,4]]},"DOI":"10.1007\/s10817-005-5204-9","type":"journal-article","created":{"date-parts":[[2006,6,15]],"date-time":"2006-06-15T08:40:18Z","timestamp":1150360818000},"page":"209-238","source":"Crossref","is-referenced-by-count":51,"title":["Combining Nonstably Infinite Theories"],"prefix":"10.1007","volume":"34","author":[{"given":"Cesare","family":"Tinelli","sequence":"first","affiliation":[]},{"given":"Calogero G.","family":"Zarba","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,6,14]]},"reference":[{"key":"5204_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F. and Tinelli, C.: A new approach for combining decision procedure for the word problem, and its connection to the Nelson\u2013Oppen combination method, in W. McCune (ed.), Automated Deduction \u2013 CADE-14, Lecture Notes in Comput. Sci. 1249, Springer, 1997,pp. 19\u201333.","DOI":"10.1007\/3-540-63104-6_3"},{"key":"5204_CR2","unstructured":"Barrett, C. W., Dill, D. L. and Stump, A.: A generalization of Shostak's method for combining decision procedures, in A. Armando (ed.), Frontiers of Combining Systems, Lecture Notes in Comput. Sci. 2309, Springer, 2002, pp. 132\u2013146."},{"key":"5204_CR3","doi-asserted-by":"crossref","first-page":"342","DOI":"10.1007\/BF01459101","volume":"99","author":"P. Bernays","year":"1928","unstructured":"Bernays, P. and Sch\u00f6nfinkel, M.: Zum Entscheidungsproblem der mathematischen Logic, Math. Ann. 99 (1928), 342\u2013372.","journal-title":"Math. Ann."},{"key":"5204_CR4","unstructured":"Cantone, D. and Zarba, C. G.: A decision procedure for monotone functions over lattices, in F. Buccafurri (ed.), Joint Conference on Declarative Programming APPIA-GULP-PRODE 2003, pp. 1\u201312."},{"key":"5204_CR5","doi-asserted-by":"crossref","unstructured":"Craigen, D., Kromodimoeljo, S., Meisels, I., Pase, B. and Saaltink, M.: EVES: An overview, in S. Prehen and H. Toetenel (eds.), Formal Software Development Methods, Lecture Notes in Comput. Sci. 552, Springer, 1991, pp. 389\u2013405.","DOI":"10.1007\/3-540-54834-3_24"},{"key":"5204_CR6","unstructured":"Detlefs, D., Nelson, G. and Saxe, J. B.: Simplify: A theorem prover for program checking, Technical Report HPL-2\u20133-148, HP Laboratories, Palo Alto, CA, 2003."},{"key":"5204_CR7","doi-asserted-by":"crossref","unstructured":"Ganzinger, H.: Shostak light, in A. Voronkov (ed.), Automated Deduction \u2013 CADE-18, Lecture Notes in Comput. Sci. 2392, Springer, 2002, pp. 332\u2013346.","DOI":"10.1007\/3-540-45620-1_28"},{"key":"5204_CR8","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Sofronie-Stokkermans, V. and Waldmann, U.: Modular proof systems for partial functions with weak equality, in D. Basin and M. Rusinowitch (eds.), Automated Reasoning, Lecture Notes in Comput. Sci. 3097, Springer, 2004, pp. 168\u2013182.","DOI":"10.1007\/978-3-540-25984-8_10"},{"key":"5204_CR9","unstructured":"Garey, M. R. and Johnson, D. S.: Computers and Intractability, W. H. Freeman & Co., 1979."},{"key":"5204_CR10","doi-asserted-by":"crossref","unstructured":"Ghilardi, S.: Quantifier elimination and provers integration, in I. Dahn and L. Vigneron (eds.), First Order Theorem Proving, Electronic Notes in Theoret. Comput. Sci. 86.1, Elsevier, 2003.","DOI":"10.1016\/S1571-0661(04)80650-9"},{"key":"5204_CR11","unstructured":"Hodges, W.: A Shorter Model Theory, Cambridge University Press, 1997."},{"key":"5204_CR12","unstructured":"Levy, B., Filippenko, I., Marcus, L. and Menas, T.: Using the state delta verification system (SDVS) for hardware verification, in T. F. Melham, V. Stavridou and R. T. Boute (eds.), Theorem Prover in Circuit Design: Theory, Practice and Experience, Elsevier Science, 1992, pp. 337\u2013360."},{"key":"5204_CR13","unstructured":"Manna, Z. and Zarba, C. G.: Combining decision procedures, in Formal Methods at the Cross Roads: From Panacea to Foundational Support, Lecture Notes in Comput. Sci. 2757, Springer, 2003, pp. 381\u2013422."},{"key":"5204_CR14","unstructured":"Nelson, G.: Techniques for program verification, Technical Report CSL-81-10, Xerox Palo Alto Research Center, 1981."},{"issue":"2","key":"5204_CR15","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G. and Oppen, D. C.: Simplification by cooperating decision procedures, ACM Trans. on Programming Languages and Systems 1(2) (1979), 245\u2013257.","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"5204_CR16","doi-asserted-by":"crossref","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 combination of theories, Theoret. Comput. Sci. 12 (1980), 291\u2013302.","journal-title":"Theoret. Comput. Sci."},{"key":"5204_CR17","unstructured":"Pnueli, A., Rodeh, Y., Strichman, O. and Siegel, M.: Deciding equality formulas by small domains instantiations, in N. Halbwachs and D. Peled (eds.), Computer Aided Verification, Lecture Notes in Comput. Sci. 1633, Springer, 1999, pp. 455\u2013469."},{"key":"5204_CR18","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1112\/plms\/s2-30.1.264","volume":"30","author":"F. P. Ramsey","year":"1930","unstructured":"Ramsey, F. P.: On a problem in formal logic, Proc. London Math. Soc. 30 (1930), 264\u2013286.","journal-title":"Proc. London Math. Soc."},{"key":"5204_CR19","doi-asserted-by":"crossref","unstructured":"Ringeissen, C.: Cooperation of decision procedures for the satisfiability problem, in F. Baader and K. U. Schulz (eds.), Frontiers of Combining Systems, Applied Logic Series 3, Kluwer Academic Publishers, 1996, pp. 121\u2013140.","DOI":"10.1007\/978-94-009-0349-4_6"},{"key":"5204_CR20","doi-asserted-by":"crossref","unstructured":"Stump, A., Barret, C. W. and Dill, D. L.: CVC: A cooperating validity checker, in E. Brinksma and K. G. Larsen (eds.), Computer Aided Verification, Lecture Notes in Comput. Sci. 2404, 2002, pp. 500\u2013504.","DOI":"10.1007\/3-540-45657-0_40"},{"issue":"1","key":"5204_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1022587501759","volume":"30","author":"C. Tinelli","year":"2003","unstructured":"Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing, J. Automated Reasoning 30(1) (2003), 1\u201331.","journal-title":"J. Automated Reasoning"},{"key":"5204_CR22","doi-asserted-by":"crossref","unstructured":"Tinelli, C. and Harandi, M. T.: A new correctness proof of the Nelson\u2013Oppen combination procedure, in F. Baader and K. U. Schulz (eds.), Frontiers of Combining Systems, Applied Logic Series 3, Kluwer Academic Publishers, 1996, pp. 103\u2013120.","DOI":"10.1007\/978-94-009-0349-4_5"},{"issue":"1","key":"5204_CR23","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/S0304-3975(01)00332-2","volume":"290","author":"C. Tinelli","year":"2003","unstructured":"Tinelli, C. and Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures, Theoret. Comput. Sci. 290(1) (2003), 291\u2013353.","journal-title":"Theoret. Comput. Sci."},{"key":"5204_CR24","doi-asserted-by":"crossref","unstructured":"Tinelli, C. and Zarba, C. G.: Combining non-stably infinite theories, in I. Dahn and L. Vigneron (eds.), First Order Theorem Proving, Electronic Notes in Theoret. Comput. Sci. 86.1, Elsevier, 2003.","DOI":"10.1016\/S1571-0661(04)80651-0"},{"key":"5204_CR25","unstructured":"Zarba, C. G.: Combining lists with integers, in R. Gor\u00e9, A. Leitsch and T. Nipkow (eds.), Automated Reasoning: Short Papers, Technical Report DII 11\/01, Universit\u00e0 di Siena, Italy, 2001, pp. 170\u2013179."},{"key":"5204_CR26","doi-asserted-by":"crossref","unstructured":"Zarba, C. G.: Combining multisets with integers, in A. Voronkov (ed.), Automated Deduction \u2013 CADE-18, Lecture Notes in Comput. Sci. 2392, Springer, 2002, pp. 363\u2013376.","DOI":"10.1007\/3-540-45620-1_30"},{"key":"5204_CR27","doi-asserted-by":"crossref","unstructured":"Zarba, C. G.: Combining sets with integers, in A. Armando (ed.), Frontiers of Combining Systems, Lecture Notes in Comput. Sci. 2309, Springer, 2002, pp. 103\u2013116.","DOI":"10.1007\/3-540-45988-X_9"},{"key":"5204_CR28","unstructured":"Zarba, C. G.: C-tableaux, Technical Report RR-5229, INRIA, 2004."},{"key":"5204_CR29","unstructured":"Zarba, C. G.: The combination problem in automated reasoning, Ph.D. thesis, Stanford University, 2004."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-5204-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-005-5204-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-005-5204-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:21:45Z","timestamp":1559251305000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-005-5204-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,4]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2005,4]]}},"alternative-id":["5204"],"URL":"https:\/\/doi.org\/10.1007\/s10817-005-5204-9","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,4]]}}}