{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,23]],"date-time":"2025-12-23T15:38:26Z","timestamp":1766504306127},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540290513"},{"type":"electronic","value":"9783540317302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11559306_3","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T12:50:36Z","timestamp":1127825436000},"page":"48-64","source":"Crossref","is-referenced-by-count":37,"title":["Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic"],"prefix":"10.1007","author":[{"given":"Silvio","family":"Ranise","sequence":"first","affiliation":[]},{"given":"Christophe","family":"Ringeissen","sequence":"additional","affiliation":[]},{"given":"Calogero G.","family":"Zarba","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11559306_2","volume-title":"Frontiers of Combining Systems","author":"F. Baader","year":"2005","unstructured":"Baader, F., Ghilardi, S.: Connecting many-sorted structures and theories through adjoint functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS, vol.\u00a03717, pp. 31\u201347. Springer, Heidelberg (2005)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/11532231_21","volume-title":"Automated Deduction \u2013 CADE-20","author":"F. Baader","year":"2005","unstructured":"Baader, F., Ghilardi, S.: Connecting many-sorted theories. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol.\u00a03632, pp. 278\u2013294. Springer, Heidelberg (2005)"},{"issue":"1","key":"3_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(96)00039-4","volume":"165","author":"M. Bidoit","year":"1996","unstructured":"Bidoit, M., Hennicker, R.: Behavioural theories and the proof of behavioural properties. Theoretical Computer Science\u00a0165(1), 3\u201355 (1996)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"3_CR4","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1590\/S0104-65002003000300003","volume":"9","author":"J.-F. Couchot","year":"2004","unstructured":"Couchot, J.-F., D\u00e9harbe, D., Giorgetti, A., Ranise, S.: Scalable automated proving and debugging of set-based specifications. Journal of the Brazilian Computer Society\u00a09(2), 17\u201336 (2004)","journal-title":"Journal of the Brazilian Computer Society"},{"key":"3_CR5","first-page":"220","volume-title":"Software Engineering and Formal Methods","author":"D. D\u00e9harbe","year":"2003","unstructured":"D\u00e9harbe, D., Ranise, S.: Light-weight theorem proving for debugging and verifying units of code. In: Software Engineering and Formal Methods, pp. 220\u2013228. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Fontaine, P., Gribomont, P.: Combining non-stably infinite, non-first order theories. In: Ranise, S., Tinelli, C. (eds.) Pragmatics of Decision Procedures in Automated Reasoning (2004)","DOI":"10.1016\/j.entcs.2004.06.066"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-540-32275-7_4","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. Fontaine","year":"2005","unstructured":"Fontaine, P., Ranise, S., Zarba, C.G.: Combining lists with non-stably infinite theories. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol.\u00a03452, pp. 51\u201366. Springer, Heidelberg (2005)"},{"key":"3_CR8","unstructured":"Ganesh, V., Berezin, S., Dill, D.L.: A decision procedure for fixed-width bit-vectors (2005) (Unpublished)"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","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, vol.\u00a02392, pp. 332\u2013346. Springer, Heidelberg (2002)"},{"key":"3_CR10","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. Technical report, INRIA, Also published as Technical Report at Department of Computer Science, University of New Mexico (2005). Electronically available at http:\/\/www.inria.fr\/rrrt\/index.en.html , http:\/\/www.inria.fr\/rrrt\/index.en.html"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/11532231_16","volume-title":"Automated Deduction \u2013 CADE-20","author":"V. Sofronie-Stokkermans","year":"2005","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol.\u00a03632, pp. 219\u2013234. Springer, Heidelberg (2005)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-540-30227-8_53","volume-title":"Logics in Artificial Intelligence","author":"C. Tinelli","year":"2004","unstructured":"Tinelli, C., Zarba, C.G.: Combining decision procedures for sorted theories. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS, vol.\u00a03229, pp. 641\u2013653. Springer, Heidelberg (2004)"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. Journal of Automated Reasoning (2005) (To appear)","DOI":"10.1007\/s10817-005-5204-9"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","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, vol.\u00a02392, pp. 363\u2013376. Springer, Heidelberg (2002)"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","first-page":"762","volume-title":"Verification: Theory and Practice","author":"C.G. Zarba","year":"2004","unstructured":"Zarba, C.G.: Combining sets with elements. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 762\u2013782. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11559306_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,4]],"date-time":"2023-05-04T19:36:49Z","timestamp":1683229009000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11559306_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540290513","9783540317302"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/11559306_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}