{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:31:01Z","timestamp":1767929461230,"version":"3.49.0"},"reference-count":16,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,3,11]],"date-time":"2017-03-11T00:00:00Z","timestamp":1489190400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia (PT)","award":["UID\/MAT\/04561\/2013"],"award-info":[{"award-number":["UID\/MAT\/04561\/2013"]}]},{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["SRFH\/BD\/52243\/2013"],"award-info":[{"award-number":["SRFH\/BD\/52243\/2013"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,2]]},"DOI":"10.1007\/s10817-017-9411-y","type":"journal-article","created":{"date-parts":[[2017,3,11]],"date-time":"2017-03-11T15:55:25Z","timestamp":1489247725000},"page":"221-236","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Many-Sorted Equivalence of Shiny and Strongly Polite Theories"],"prefix":"10.1007","volume":"60","author":[{"given":"Filipe","family":"Casal","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1239-8496","authenticated-orcid":false,"given":"Jo\u00e3o","family":"Rasga","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,3,11]]},"reference":[{"key":"9411_CR1","doi-asserted-by":"crossref","unstructured":"Areces, C., Fontaine, P.: Combining theories: the ackerman and guarded fragments. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) Frontiers of Combining Systems. FroCoS 2011. Lecture Notes in Computer Science, vol. 6989. Springer, Berlin, Heidelberg (2011)","DOI":"10.1007\/978-3-642-24364-6_4"},{"key":"9411_CR2","doi-asserted-by":"crossref","unstructured":"Casal, F., Rasga, J.: Revisiting the equivalence of shininess and politeness. In: Proceedings of the Nineteenth International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u20192013), Volume 8312 of LNCS, pp. 198\u2013212 (2013)","DOI":"10.1007\/978-3-642-45221-5_15"},{"key":"9411_CR3","doi-asserted-by":"crossref","unstructured":"Chocron, P., Fontaine, P., Ringeissen, C.: A gentle non-disjoint combination of satisfiability procedures. In: International Joint Conference on Automated Reasoning, pp. 122\u2013136. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-08587-6_9"},{"key":"9411_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2181-2","volume-title":"Ideals, Varieties, and Algorithms","author":"D Cox","year":"1992","unstructured":"Cox, D., Little, J., O\u2019shea, D.: Ideals, Varieties, and Algorithms, vol. 3. Springer, New York (1992)"},{"issue":"3","key":"9411_CR5","doi-asserted-by":"crossref","first-page":"597","DOI":"10.1137\/070697720","volume":"40","author":"C Daskalakis","year":"2011","unstructured":"Daskalakis, C., Karp, R.M., Mossel, E., Riesenfeld, S.J., Verbin, E.: Sorting and selection in posets. SIAM J. Comput. 40(3), 597\u2013622 (2011)","journal-title":"SIAM J. Comput."},{"key":"9411_CR6","doi-asserted-by":"crossref","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Elsevier Science (2001)","DOI":"10.1016\/B978-0-08-049646-7.50005-9"},{"key":"9411_CR7","doi-asserted-by":"crossref","unstructured":"Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: Ghilardi, S., Sebastiani, R. (eds.) Frontiers of Combining Systems. FroCoS 2009. Lecture Notes in Computer Science, vol. 5749. Springer, Berlin, Heidelberg (2009)","DOI":"10.1007\/978-3-642-04222-5_16"},{"issue":"4","key":"9411_CR8","doi-asserted-by":"crossref","first-page":"473","DOI":"10.1007\/BF01208503","volume":"36","author":"D Hilbert","year":"1890","unstructured":"Hilbert, D.: \u00dcber die Theorie der algebraischen Formen. Math. Ann. 36(4), 473\u2013534 (1890)","journal-title":"Math. Ann."},{"issue":"6","key":"9411_CR9","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1145\/362248.362272","volume":"16","author":"JE Hopcroft","year":"1973","unstructured":"Hopcroft, J.E., Tarjan, R.E.: Efficient algorithms for graph manipulation [H] (Algorithm 447). Commun. ACM 16(6), 372\u2013378 (1973)","journal-title":"Commun. ACM"},{"key":"9411_CR10","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., Barrett, C.: Polite theories revisited. In: Proceedings of the Seventeenth International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u20192010), Volume 6397 of LNCS, pp. 402\u2013416 (2010)","DOI":"10.1007\/978-3-642-16242-8_29"},{"key":"9411_CR11","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., Barrett, C.: Polite theories revisited. Technical Report TR2010-922, Department of Computer Science, New York University (2010)","DOI":"10.1007\/978-3-642-16242-8_29"},{"issue":"2","key":"9411_CR12","doi-asserted-by":"crossref","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 Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9411_CR13","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"DC Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12, 291\u2013302 (1980)","journal-title":"Theor. Comput. Sci."},{"key":"9411_CR14","doi-asserted-by":"crossref","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Proceedings of the Fifth International Workshop on Frontiers of Combining Systems (FroCoS\u20192005), Volume 3717 of LNAI, pp. 48\u201364 (2005)","DOI":"10.1007\/11559306_3"},{"key":"9411_CR15","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson\u2013Oppen combination procedure. In: Proceedings of the First International Workshop on Frontiers of Combining Systems (FroCoS\u20191996), Volume 3 of Applied Logic Series, pp. 103\u2013119 (1996)","DOI":"10.1007\/978-94-009-0349-4_5"},{"issue":"3","key":"9411_CR16","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.G.: Combining non-stably infinite theories. J. Automat. Reason. 34(3), 209\u2013238 (2005)","journal-title":"J. Automat. Reason."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9411-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9411-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9411-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,19]],"date-time":"2019-09-19T12:51:14Z","timestamp":1568897474000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9411-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,11]]},"references-count":16,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,2]]}},"alternative-id":["9411"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9411-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,3,11]]}}}