{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T10:18:59Z","timestamp":1649153939205},"reference-count":20,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,5,1]],"date-time":"2003-05-01T00:00:00Z","timestamp":1051747200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3742,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,5]]},"DOI":"10.1016\/s1571-0661(04)80651-0","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"35-48","source":"Crossref","is-referenced-by-count":6,"title":["Combining Non-Stably Infinite Theories"],"prefix":"10.1016","volume":"86","author":[{"given":"Cesare","family":"Tinelli","sequence":"first","affiliation":[]},{"given":"Calogero G.","family":"Zarba","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB1","series-title":"Automated Deduction - CADE-14","first-page":"19","article-title":"A new approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method","author":"Baader","year":"1997"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB2","series-title":"Formal Software Development Methods","first-page":"389","article-title":"EVES: An overview","author":"Craigen","year":"1991"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB3","unstructured":"Detlefs, D. L., K. R. M. Leino, G. Nelson and J. B. Saxe, Extended static checking, Technical Report 159, Compaq System Research Center (1998)."},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB4","doi-asserted-by":"crossref","DOI":"10.1016\/S1571-0661(04)80650-9","article-title":"Quantifier elimination and provers integration","volume":"86","author":"Ghilardi","year":"2003","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB5","series-title":"\u201cA Shorter Model Theory,\u201d","author":"Hodges","year":"1997"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB6","series-title":"Theorem Prover in Circuit Design: Theory, Practice and Experience","first-page":"337","article-title":"Using the state delta verification system (SDVS) for hardware verification","author":"Levy","year":"1992"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB7","doi-asserted-by":"crossref","unstructured":"Manna Z. and C. G. Zarba, Combining decision procedures, in: Formal Methods at the Cross Roads: From Panacea to Foundational Support, Lecture Notes in Computer Science (2003), to appear.","DOI":"10.1007\/978-3-540-40007-3_24"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB8","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","article-title":"Simplification by cooperating decision procedures","volume":"1","author":"Nelson","year":"1979","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB9","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","article-title":"Fast decision procedures based on congruence closure","volume":"27","author":"Nelson","year":"1980","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB10","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","article-title":"Complexity, convexity and combination of theories","volume":"12","author":"Oppen","year":"1980","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB11","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1006\/jsco.1995.1053","article-title":"T-theorem proving I","volume":"20","author":"Policriti","year":"1995","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB12","series-title":"Computer Aided Verification","first-page":"500","article-title":"CVC: A cooperating validity checker","author":"Stump","year":"2002"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB13","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1023\/A:1022587501759","article-title":"Cooperation of background reasoners in theory reasoning by residue sharing","volume":"30","author":"Tinelli","year":"2003","journal-title":"Journal of Automated Reasoning"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB14","series-title":"Frontiers of Combining Systems","first-page":"103","article-title":"A new correctness proof of the Nelson-Oppen combination procedure","author":"Tinelli","year":"1996"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB15","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/S0304-3975(01)00332-2","article-title":"Unions of non-disjoint theories and combinations of satisfiability procedures","volume":"290","author":"Tinelli","year":"2003","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB16","doi-asserted-by":"crossref","unstructured":"Tinelli C. and C. G. Zarba, Combining non-stably infinite theories, Technical report, University of Iowa (2003), electronically available at ftp:\/\/ftp.cs.uiowa.edu\/pub\/tinelli\/papers\/TinZar-RR-03.pdf.","DOI":"10.1016\/S1571-0661(04)80651-0"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB17","unstructured":"Zarba, C. G., Combining lists with integers, in: R. Gor\u00e9, A. Leitsch and T. Nipkow, editors, International Joint Conference on Automated Reasoning: Short Papers, Technical Report DII 11\/01, Universit\u00e0 di Siena, 2001, pp. 170\u2013179."},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB18","series-title":"Automated Deduction - CADE-18","first-page":"363","article-title":"Combining multisets with integers","author":"Zarba","year":"2002"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB19","series-title":"Frontiers of Combining Systems","first-page":"103","article-title":"Combining sets with integers","author":"Zarba","year":"2002"},{"key":"10.1016\/S1571-0661(04)80651-0_NEWBIB20","series-title":"Automated Reasoning with Analytical Tableaux and Related Methods","first-page":"315","article-title":"A tableau calculus for combining non-disjoint theories","author":"Zarba","year":"2002"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806510?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104806510?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,3]],"date-time":"2019-02-03T10:53:08Z","timestamp":1549191188000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104806510"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,5]]},"references-count":20,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,5]]}},"alternative-id":["S1571066104806510"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80651-0","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,5]]}}}