{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,7]],"date-time":"2024-03-07T15:43:50Z","timestamp":1709826230468},"reference-count":34,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":2476,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2007,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Basically, the connection of two many-sorted theories is obtained by taking their disjoint union, and then connecting the two parts through connection functions that must behave like homomorphisms on the shared signature. We determine conditions under which decidability of the validity of universal formulae in the component theories transfers to their connection. In addition, we consider variants of the basic connection scheme. Our results can be seen as a generalization of the so-called <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"gif\" xlink:type=\"simple\" xlink:href=\"S0022481200005351_inline01\" \/>-connection approach for combining modal logics to an algebraic setting.<\/jats:p>","DOI":"10.2178\/jsl\/1185803623","type":"journal-article","created":{"date-parts":[[2007,12,19]],"date-time":"2007-12-19T16:24:48Z","timestamp":1198081488000},"page":"535-583","source":"Crossref","is-referenced-by-count":12,"title":["Connecting many-sorted theories"],"prefix":"10.1017","volume":"72","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":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200005351_ref012","first-page":"267\u2013281","volume-title":"Proceedings of the 12th International Conference on Automated Deduction","volume":"814","author":"Domenjoud","year":"1994"},{"key":"S0022481200005351_ref006","doi-asserted-by":"crossref","first-page":"1\u201358","DOI":"10.1613\/jair.919","article-title":"Fusions of description logics and abstract description systems","volume":"16","author":"Baader","year":"2002","journal-title":"Journal of Artificial Intelligence Research"},{"key":"S0022481200005351_ref028","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80022-7"},{"key":"S0022481200005351_ref002","first-page":"31\u201347","volume-title":"Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS 2005)","volume":"3717","author":"Baader","year":"2005"},{"key":"S0022481200005351_ref014","volume-title":"Logic for computer science: Foundations of automatic theorem proving","author":"Gallier","year":"1986"},{"key":"S0022481200005351_ref033","first-page":"363\u2013376","volume-title":"Proceedings of the 18th International Conference on Automated Deduction (CADE\u201918)","volume":"2392","author":"Zarba","year":"2002"},{"key":"S0022481200005351_ref026","doi-asserted-by":"publisher","DOI":"10.4064\/cm-30-1-15-25"},{"key":"S0022481200005351_ref016","first-page":"221\u2013249","article-title":"Model-theoretic methods in combined constraint satisfiability","volume":"33","author":"Ghilardi","year":"2005","journal-title":"Journal of Automated Reasoning"},{"key":"S0022481200005351_ref018","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511551574"},{"key":"S0022481200005351_ref025","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90059-6"},{"key":"S0022481200005351_ref010","first-page":"513\u2013527","volume-title":"Proceedings of the Third International Joint Conference on Automated Reasoning","volume":"4130","author":"Bonacina","year":"2006"},{"key":"S0022481200005351_ref023","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"S0022481200005351_ref031","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00332-2"},{"key":"S0022481200005351_ref021","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066201"},{"key":"S0022481200005351_ref001","first-page":"331\u2013345","volume-title":"Proceedings of the Fourteenth International Conference on Logic Programming","author":"Ajili","year":"1997"},{"key":"S0022481200005351_ref003","first-page":"278\u2013294","volume-title":"Proceedings of the 20th International Conference on Automated Deduction (CADE-05)","volume":"3632","author":"Baader","year":"2005"},{"key":"S0022481200005351_ref004","first-page":"183\u2013197","volume-title":"Proceedings of the Second International Joint Conference on Automated Reasoning (IJCAR\u201904)","volume":"3097","author":"Baader","year":"2004"},{"key":"S0022481200005351_ref005","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.05.009"},{"key":"S0022481200005351_ref008","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3118"},{"key":"S0022481200005351_ref009","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884"},{"key":"S0022481200005351_ref011","volume-title":"Model theory","author":"Chang","year":"1990"},{"key":"S0022481200005351_ref034","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(94)00018-X"},{"key":"S0022481200005351_ref013","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00248-1"},{"key":"S0022481200005351_ref030","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022587501759"},{"key":"S0022481200005351_ref015","unstructured":"Ghilardi Silvio , Reasoners\u2019 cooperation and quantifier elimination, Technical Report 288-03, Dipartimento di Scienze dell\u2019Informazione, Universit\u00e0 degli Studi di Milano, 2003, Available on-line at http:\/\/homes.dsi.unimi.it\/\u223cghilardi\/allegati\/eqfin.ps."},{"key":"S0022481200005351_ref017","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-9936-8"},{"key":"S0022481200005351_ref019","first-page":"1469\u20131485","volume":"56","author":"Kracht","year":"1991","journal-title":"Properties of independently axiomatizable bimodal logics"},{"key":"S0022481200005351_ref020","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2004.02.002"},{"key":"S0022481200005351_ref022","first-page":"201\u2013211","volume-title":"Automated theorem proving: After 25 years","volume":"29","author":"Nelson","year":"1984"},{"key":"S0022481200005351_ref024","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(08)80145-9"},{"key":"S0022481200005351_ref027","volume-title":"Comptes rendus du congr\u00e8s de math\u00e9maticiens des pays slaves","author":"Presburger","year":"1929"},{"key":"S0022481200005351_ref029","unstructured":"Spaan Edith , Complexity of modal logics, Ph.D. thesis, Department of Mathematics and Computer Science, University of Amsterdam, The Netherlands, 1993."},{"key":"S0022481200005351_ref032","first-page":"361\u2013379","volume-title":"Advances in modal logic","author":"Wolter","year":"1998"},{"key":"S0022481200005351_ref007","first-page":"19\u201333","volume-title":"Proceedings of the 14th International Conference on Automated Deduction","volume":"1249","author":"Baader","year":"1997"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200005351","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T22:13:10Z","timestamp":1556748790000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200005351\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2007,6]]}},"alternative-id":["S0022481200005351"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1185803623","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,6]]}}}