{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:12:53Z","timestamp":1767928373118,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642452208","type":"print"},{"value":"9783642452215","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45221-5_15","type":"book-chapter","created":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T04:28:23Z","timestamp":1386217703000},"page":"198-212","source":"Crossref","is-referenced-by-count":7,"title":["Revisiting the Equivalence of Shininess and Politeness"],"prefix":"10.1007","author":[{"given":"Filipe","family":"Casal","sequence":"first","affiliation":[]},{"given":"Jo\u00e3o","family":"Rasga","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2011","unstructured":"Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanovi\u0107, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: CAV 2011. LNCS, vol.\u00a06806, pp. 171\u2013177. Springer, Heidelberg (2011)"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-31759-0_19","volume-title":"Model Checking Software","author":"J. Christ","year":"2012","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol.\u00a07385, pp. 248\u2013254. Springer, Heidelberg (2012)"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-642-16242-8_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Jovanovi\u0107","year":"2010","unstructured":"Jovanovi\u0107, D., Barrett, C.: Polite theories revisited. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 402\u2013416. Springer, Heidelberg (2010)"},{"issue":"2","key":"15_CR4","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"},{"key":"15_CR5","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"},{"key":"15_CR6","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":"15_CR7","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Proceedings of the First International Workshop on Frontiers of Combining Systems (FroCoS 1996). Applied Logic Series, vol.\u00a03, pp. 103\u2013119 (1996)","DOI":"10.1007\/978-94-009-0349-4_5"},{"key":"15_CR8","unstructured":"Tinelli, C., Harandi, M.T.: Constraint logic programming over unions of constraint theories. Journal of Functional and Logic Programming 1998(6) (1998)"},{"issue":"3","key":"15_CR9","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-45221-5_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T00:28:57Z","timestamp":1558744137000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45221-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642452208","9783642452215"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45221-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}