{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,23]],"date-time":"2025-12-23T15:37:09Z","timestamp":1766504229762,"version":"build-2065373602"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642162411"},{"type":"electronic","value":"9783642162428"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16242-8_29","type":"book-chapter","created":{"date-parts":[[2010,10,4]],"date-time":"2010-10-04T12:51:59Z","timestamp":1286196719000},"page":"402-416","source":"Crossref","is-referenced-by-count":25,"title":["Polite Theories Revisited"],"prefix":"10.1007","author":[{"given":"Dejan","family":"Jovanovi\u0107","sequence":"first","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","first-page":"21","DOI":"10.3233\/SAT190028","volume":"3","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. Journal on Satisfiability, Boolean Modeling and Computation\u00a03, 21\u201346 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"29_CR2","volume-title":"A mathematical introduction to logic","author":"H.B. Enderton","year":"1972","unstructured":"Enderton, H.B.: A mathematical introduction to logic. Academic Press, New York (1972)"},{"key":"29_CR3","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., Barrett, C.: Polite theories revisited. Technical Report TR2010-922, Department of Computer Science, New York University (January 2010)","DOI":"10.1007\/978-3-642-16242-8_29"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"602","DOI":"10.1007\/978-3-540-71209-1_47","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, S., Goel, A., Grundy, J., Tinelli, C.: Combined Satisfiability Modulo Parametric Theories. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 602\u2013617. Springer, Heidelberg (2007)"},{"issue":"2","key":"29_CR5","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":"3","key":"29_CR6","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(3), 291\u2013302 (1980)","journal-title":"Theoretical Computer Science"},{"key":"29_CR7","doi-asserted-by":"crossref","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.: Combining Data Structures with Nonstably Infinite Theories using Many-Sorted Logic. Research Report RR-5678, INRIA (2005)","DOI":"10.1007\/11559306_3"},{"key":"29_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/11559306_3","volume-title":"Frontiers of Combining Systems","author":"S. Ranise","year":"2005","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining Data Structures with Nonstably Infinite Theories Using Many-Sorted Logic. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol.\u00a03717, pp. 48\u201364. Springer, Heidelberg (2005)"},{"key":"29_CR9","first-page":"29","volume-title":"Proceedings of the 16 th IEEE Symposium on Logic in Computer Science (LICS 2001)","author":"A. Stump","year":"2001","unstructured":"Stump, A., Dill, D.L., Barrett, C.W., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings of the 16 th IEEE Symposium on Logic in Computer Science (LICS 2001), June 2001, pp. 29\u201337. IEEE Computer Society, Boston (June 2001)"},{"key":"29_CR10","series-title":"Applied Logic","doi-asserted-by":"publisher","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\u2013Oppen combination procedure. In: Frontiers of Combining Systems. Applied Logic, pp. 103\u2013120. Kluwer Academic Publishers, Dordrecht (1996)"},{"key":"29_CR11","series-title":"Lecture Notes in Artificial Intelligence","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.: Combining decision procedures for sorted theories. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol.\u00a03229, pp. 641\u2013653. Springer, Heidelberg (2004)"},{"key":"29_CR12","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Zarba, C.: Combining decision procedures for theories in sorted logics. Technical Report 04-01, Department of Computer Science, The University of Iowa (February 2004)","DOI":"10.1007\/978-3-540-30227-8_53"},{"issue":"3","key":"29_CR13","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C. Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. Journal of Automated Reasoning\u00a034(3), 209\u2013238 (2005)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16242-8_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,12]],"date-time":"2020-06-12T10:18:27Z","timestamp":1591957107000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16242-8_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642162411","9783642162428"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16242-8_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}