{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:17:05Z","timestamp":1725560225953},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540280057"},{"type":"electronic","value":"9783540318644"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_21","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T14:56:52Z","timestamp":1279724212000},"page":"278-294","source":"Crossref","is-referenced-by-count":8,"title":["Connecting Many-Sorted Theories"],"prefix":"10.1007","author":[{"given":"Franz","family":"Baader","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","first-page":"331","volume-title":"Proceedings of Fourteenth International Conference on Logic Programming","author":"F. Ajili","year":"1997","unstructured":"Ajili, F., Kirchner, C.: A modular framework for the combination of symbolic and built-in constraints. In: Proceedings of Fourteenth International Conference on Logic Programming, Leuven, Belgium, pp. 331\u2013345. The MIT Press, Cambridge (1997)"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Baader, F., Ghilardi, S.: Connecting many-sorted theories. LTCS-Report LTCS-05-04, TU Dresden, Germany, See (2005), http:\/\/lat.inf.tu-dresden.de\/research\/reports.html","DOI":"10.25368\/2022.147"},{"key":"21_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-25984-8_11","volume-title":"Automated Reasoning","author":"F. Baader","year":"2004","unstructured":"Baader, F., Ghilardi, S., Tinelli, C.: A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 183\u2013197. Springer, Heidelberg (2004)"},{"key":"21_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1080\/088395102753365771","volume":"16","author":"F. Baader","year":"2002","unstructured":"Baader, F., Lutz, C., Sturm, H., Wolter, F.: Fusions of description logics and abstract description systems. Journal of Artificial Intelligence Research\u00a016, 1\u201358 (2002)","journal-title":"Journal of Artificial Intelligence Research"},{"key":"21_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/3-540-63104-6_3","volume-title":"Proceedings of the 14th International Conference on Automated Deduction","author":"F. Baader","year":"1997","unstructured":"Baader, F., Tinelli, C.: A new approach for combining decision procedures for the word problem, and its connection to the Nelson-Oppen combination method. In: Proceedings of the 14th International Conference on Automated Deduction, Townsville (Australia). LNCS (LNAI), vol.\u00a01249, pp. 19\u201333. Springer, Heidelberg (1997)"},{"issue":"2","key":"21_CR6","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1006\/inco.2001.3118","volume":"178","author":"F. Baader","year":"2002","unstructured":"Baader, F., Tinelli, C.: Deciding the word problem in the union of equational theories. Information and Computation\u00a0178(2), 346\u2013390 (2002)","journal-title":"Information and Computation"},{"key":"21_CR7","volume-title":"Model Theory","author":"C.-C. Chang","year":"1990","unstructured":"Chang, C.-C., Keisler, H.J.: Model Theory, 3rd edn. North-Holland, Amsterdam (1990)","edition":"3"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/3-540-58156-1_19","volume-title":"Automated Deduction - CADE-12","author":"E. Domenjoud","year":"1994","unstructured":"Domenjoud, E., Klay, F., Ringeissen, C.: Combination techniques for non-disjoint equational theories. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 267\u2013281. Springer, Heidelberg (1994)"},{"key":"21_CR9","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0304-3975(01)00248-1","volume":"294","author":"C. Fiorentini","year":"2003","unstructured":"Fiorentini, C., Ghilardi, S.: Combining word problems through rewriting in categories with products. Theoretical Computer Science\u00a0294, 103\u2013149 (2003)","journal-title":"Theoretical Computer Science"},{"key":"21_CR10","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"J.H. Gallier","year":"1986","unstructured":"Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, New York (1986)"},{"issue":"3\u20134","key":"21_CR11","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10817-004-6241-5","volume":"33","author":"S. Ghilardi","year":"2004","unstructured":"Ghilardi, S.: Model-theoretic methods in combined constraint satisfiability. Journal of Automated Reasoning\u00a033(3\u20134), 221\u2013249 (2004)","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"21_CR12","doi-asserted-by":"publisher","first-page":"1469","DOI":"10.2307\/2275487","volume":"56","author":"M. Kracht","year":"1991","unstructured":"Kracht, M., Wolter, F.: Properties of independently axiomatizable bimodal logics. The Journal of Symbolic Logic\u00a056(4), 1469\u20131485 (1991)","journal-title":"The Journal of Symbolic Logic"},{"key":"21_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artint.2004.02.002","volume":"156","author":"O. Kutz","year":"2004","unstructured":"Kutz, O., Lutz, C., Wolter, F., Zakharyaschev, M.: $\\mathcal{E}$ -connections of abstract description systems. Artificial Intelligence\u00a0156, 1\u201373 (2004)","journal-title":"Artificial Intelligence"},{"key":"21_CR14","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0066201","volume-title":"First-Order Categorical Logic","author":"M. Makkai","year":"1977","unstructured":"Makkai, M., Reyes, G.E.: First-Order Categorical Logic. Lecture Notes in Mathematics, vol.\u00a0611. Springer, Berlin (1977)"},{"key":"21_CR15","series-title":"Contemporary Mathematics","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1090\/conm\/029\/11","volume-title":"Automated Theorem Proving: After 25 Years","author":"G. Nelson","year":"1984","unstructured":"Nelson, G.: Combining satisfiability procedures by equality-sharing. In: Bledsoe, W.W., Loveland, D.W. (eds.) Automated Theorem Proving: After 25 Years. Contemporary Mathematics, vol.\u00a029, pp. 201\u2013211. American Mathematical Society, Providence (1984)"},{"issue":"2","key":"21_CR16","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 Trans.\u00a0on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans.\u00a0on Programming Languages and Systems"},{"key":"21_CR17","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1016\/S0747-7171(08)80145-9","volume":"12","author":"T. Nipkow","year":"1991","unstructured":"Nipkow, T.: Combining matching algorithms: The regular case. Journal of Symbolic Computation\u00a012, 633\u2013653 (1991)","journal-title":"Journal of Symbolic Computation"},{"key":"21_CR18","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"},{"issue":"1","key":"21_CR19","doi-asserted-by":"crossref","first-page":"15","DOI":"10.4064\/cm-30-1-15-25","volume":"30","author":"D. Pigozzi","year":"1974","unstructured":"Pigozzi, D.: The join of equational theories. Colloquium Mathematicum\u00a030(1), 15\u201325 (1974)","journal-title":"Colloquium Mathematicum"},{"key":"21_CR20","unstructured":"Spaan, E.: Complexity of Modal Logics. PhD thesis, Department of Mathematics and Computer Science, University of Amsterdam, The Netherlands (1993)"},{"issue":"1","key":"21_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1023\/A:1022587501759","volume":"30","author":"C. Tinelli","year":"2003","unstructured":"Tinelli, C.: Cooperation of background reasoners in theory reasoning by residue sharing. Journal of Automated Reasoning\u00a030(1), 1\u201331 (2003)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"21_CR22","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/S0304-3975(01)00332-2","volume":"290","author":"C. Tinelli","year":"2003","unstructured":"Tinelli, C., Ringeissen, C.: Unions of non-disjoint theories and combinations of satisfiability procedures. Theoretical Computer Science\u00a0290(1), 291\u2013353 (2003)","journal-title":"Theoretical Computer Science"},{"key":"21_CR23","unstructured":"Wolter, F.: Fusions of modal logics revisited. In: Advances in Modal Logic. CSLI, Stanford, CA (1998)"},{"key":"21_CR24","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-45620-1_30","volume-title":"Automated Deduction - CADE-18","author":"C. Zarba","year":"2002","unstructured":"Zarba, C.: Combining multisets with integers. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 363\u2013376. Springer, Heidelberg (2002)"},{"issue":"2","key":"21_CR25","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/0168-0072(94)00018-X","volume":"71","author":"M.W. Zawadowski","year":"1995","unstructured":"Zawadowski, M.W.: Descent and duality. Ann. Pure Appl. Logic\u00a071(2), 131\u2013188 (1995)","journal-title":"Ann. Pure Appl. Logic"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,2]],"date-time":"2023-06-02T02:57:14Z","timestamp":1685674634000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/11532231_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}