{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:35:44Z","timestamp":1750307744986,"version":"3.41.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2008,3,1]],"date-time":"2008-03-01T00:00:00Z","timestamp":1204329600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2008,3]]},"abstract":"<jats:p>We define a general notion of a fragment within higher-order type theory; a procedure for constraint satisfiability in combined fragments is outlined, following Nelson-Oppen schema. The procedure is in general only sound, but it becomes terminating and complete when the shared fragment enjoys suitable noetherianity conditions and admits an abstract version of a \u201cKeisler-Shelah-like\u201d isomorphism theorem. We show that this general decidability transfer result covers recent work on combination in first-order theories as well as in various intensional logics such as description, modal, and temporal logics.<\/jats:p>","DOI":"10.1145\/1342991.1342992","type":"journal-article","created":{"date-parts":[[2008,4,8]],"date-time":"2008-04-08T15:40:00Z","timestamp":1207669200000},"page":"1-54","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["A comprehensive combination framework"],"prefix":"10.1145","volume":"9","author":[{"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano, Milan, Italy"}]},{"given":"Enrica","family":"Nicolini","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano, Milan, Italy"}]},{"given":"Daniele","family":"Zucchelli","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano, Milan, Italy and LORIA &amp; INRIA-Lorraine"}]}],"member":"320","published-online":{"date-parts":[[2008,4,7]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1004275029985"},{"volume-title":"Handbook of Automated Reasoning","author":"Andrews P. B.","key":"e_1_2_1_2_1","unstructured":"Andrews , P. B. 2001. Classical type theory . In Handbook of Automated Reasoning , A. Robinson and A. Voronkov, Eds. Vol. 2. Elsevier and MIT Press , Cambridge, MA , Chapter 15, 966--1007. Andrews, P. B. 2001. Classical type theory. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. 2. Elsevier and MIT Press, Cambridge, MA, Chapter 15, 966--1007."},{"volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof","author":"Andrews P. B.","key":"e_1_2_1_3_1","unstructured":"Andrews , P. B. 2002. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof , second ed. Applied Logic Series, vol. 27 . Kluwer Academic Publishers , Dordrecht (Holland). Andrews, P. B. 2002. An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, second ed. Applied Logic Series, vol. 27. Kluwer Academic Publishers, Dordrecht (Holland)."},{"volume-title":"2003. The Description Logic Handbook","author":"Baader F.","key":"e_1_2_1_4_1","unstructured":"Baader , F. , Calvanese , D. , McGuinness , D. L. , Nardi , D. , and Patel-Schneider , P. F. , Eds. 2003. The Description Logic Handbook . Cambridge University Press , Cambridge (UK). Theory, implementation, and applications. Baader, F., Calvanese, D., McGuinness, D. L., Nardi, D., and Patel-Schneider, P. F., Eds. 2003. The Description Logic Handbook. Cambridge University Press, Cambridge (UK). Theory, implementation, and applications."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11559306_2"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_21"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.05.009"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI","volume":"1","author":"Baader F.","year":"1991","unstructured":"Baader , F. and Hanschke , P . 1991. A scheme for integrating concrete domains into concept languages . In Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI 1991 ). Vol. 1 . (Sydney, Australia). Morgan-Kaufman, San Francisco, CA, 452--457. Baader, F. and Hanschke, P. 1991. A scheme for integrating concrete domains into concept languages. In Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI 1991). Vol. 1. (Sydney, Australia). Morgan-Kaufman, San Francisco, CA, 452--457."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622407.1622408"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press Cambridge UK.   Baader F. and Nipkow T. 1998. Term Rewriting and All That. Cambridge University Press Cambridge UK.","DOI":"10.1017\/CBO9781139172752"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.3118"},{"key":"e_1_2_1_12_1","unstructured":"Baumgartner P. Furbach U. and Petermann U. 1992. A unified approach to theory reasoning. Res. Rep. 15--92 Universit\u00e4t Koblenz-Landau Koblenz (Germany). Fachberichte Informatik.  Baumgartner P. Furbach U. and Petermann U. 1992. A unified approach to theory reasoning. Res. Rep. 15--92 Universit\u00e4t Koblenz-Landau Koblenz (Germany). Fachberichte Informatik."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_42"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"B\u00f6rger E. Gr\u00e4del E. and Gurevich Y. 2001. The classical decision problem. Universitext. Springer-Verlag Berlin (Germany). (Reprint of the 1997 original.)  B\u00f6rger E. Gr\u00e4del E. and Gurevich Y. 2001. The classical decision problem. Universitext. Springer-Verlag Berlin (Germany). (Reprint of the 1997 original.)","DOI":"10.1007\/978-3-642-59207-2"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.05.011"},{"key":"e_1_2_1_16_1","unstructured":"Chang C.-C. and Keisler H. J. 1990. Model Theory third ed. North-Holland Amsterdam Holland.  Chang C.-C. and Keisler H. J. 1990. Model Theory third ed. North-Holland Amsterdam Holland."},{"volume-title":"Canonical Forms in Finitely Presented Algebras. Research Notes in Theoretical Computer Science","author":"Chenadec P. L.","key":"e_1_2_1_17_1","unstructured":"Chenadec , P. L. 1986. Canonical Forms in Finitely Presented Algebras. Research Notes in Theoretical Computer Science . Pitman Publishing Ltd ., London, UK. Chenadec, P. L. 1986. Canonical Forms in Finitely Presented Algebras. Research Notes in Theoretical Computer Science. Pitman Publishing Ltd., London, UK."},{"edition":"2","volume-title":"Cox, D., Little, J., and O'Shea, D. 1997. Ideals, Varieties, and Algorithms","key":"e_1_2_1_18_1","unstructured":"Cox, D., Little, J., and O'Shea, D. 1997. Ideals, Varieties, and Algorithms , 2 nd ed. Undergraduate Texts in Mathematics. Springer-Verlag , New York. Cox, D., Little, J., and O'Shea, D. 1997. Ideals, Varieties, and Algorithms, 2nd ed. Undergraduate Texts in Mathematics. Springer-Verlag, New York."},{"volume-title":"Handbook of Automated Reasoning","author":"Dowek G.","key":"e_1_2_1_19_1","unstructured":"Dowek , G. 2001. Higher order unification and matching . In Handbook of Automated Reasoning , A. Robinson and A. Voronkov, Eds. Vol. 2. Elsevier and MIT Press , Chapter 16, 1009--1062. Dowek, G. 2001. Higher order unification and matching. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Vol. 2. Elsevier and MIT Press, Chapter 16, 1009--1062."},{"key":"e_1_2_1_20_1","volume-title":"Resolution Methods for the Decision Problem. Lecture Notes in Computer Science","volume":"679","author":"Ferm\u00fcller C.","unstructured":"Ferm\u00fcller , C. , Leitsch , A. , Tammet , T. , and Zamov , N . 1993 . Resolution Methods for the Decision Problem. Lecture Notes in Computer Science , vol. 679 . Springer-Verlag, Berlin, Germany. Ferm\u00fcller, C., Leitsch, A., Tammet, T., and Zamov, N. 1993. Resolution Methods for the Decision Problem. Lecture Notes in Computer Science, vol. 679. Springer-Verlag, Berlin, Germany."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00248-1"},{"key":"e_1_2_1_22_1","series-title":"Lecture Notes in Mathemathics","volume-title":"Proceedings of the Logic Colloquium (Boston, MA)","author":"Friedman H.","unstructured":"Friedman , H. 1975. Equality between functionals . In Proceedings of the Logic Colloquium (Boston, MA) . Lecture Notes in Mathemathics , vol. 453 . Springer-Verlag , New York , 22--37. Friedman, H. 1975. Equality between functionals. In Proceedings of the Logic Colloquium (Boston, MA). Lecture Notes in Mathemathics, vol. 453. Springer-Verlag, New York, 22--37."},{"key":"e_1_2_1_23_1","volume-title":"Many-Dimensional Modal Logics: Theory and Applications. Studies in Logic and the Foundations of Mathematics","volume":"148","author":"Gabbay D. M.","unstructured":"Gabbay , D. M. , Kurucz , A. , Wolter , F. , and Zakharyaschev , M . 2003 . Many-Dimensional Modal Logics: Theory and Applications. Studies in Logic and the Foundations of Mathematics , vol. 148 . North-Holland Publishing Co., Amsterdam, Holland. Gabbay, D. M., Kurucz, A., Wolter, F., and Zakharyaschev, M. 2003. Many-Dimensional Modal Logics: Theory and Applications. Studies in Logic and the Foundations of Mathematics, vol. 148. North-Holland Publishing Co., Amsterdam, Holland."},{"volume-title":"Proceedings of the 14th Symposium on Logic in Computer Science (LICS 1999)","author":"Ganzinger H.","key":"e_1_2_1_24_1","unstructured":"Ganzinger , H. and de Nivelle, H. 1999. A superposition decision procedure for the guarded fragment with equality . In Proceedings of the 14th Symposium on Logic in Computer Science (LICS 1999) (Trento, Italy). IEEE Computer Society Press, Los Alamitos, CA, 295--303. Ganzinger, H. and de Nivelle, H. 1999. A superposition decision procedure for the guarded fragment with equality. In Proceedings of the 14th Symposium on Logic in Computer Science (LICS 1999) (Trento, Italy). IEEE Computer Society Press, Los Alamitos, CA, 295--303."},{"key":"e_1_2_1_25_1","volume-title":"Notes of the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR","author":"Ganzinger H.","year":"2005","unstructured":"Ganzinger , H. , Rue\u00df , H. , and Shankar , N . 2005. Modularity and refinement in inference systems . In Notes of the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005 ), (Edinburgh, Scotland). Ganzinger, H., Rue\u00df, H., and Shankar, N. 2005. Modularity and refinement in inference systems. In Notes of the 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning (PDPAR 2005), (Edinburgh, Scotland)."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-004-6241-5"},{"key":"e_1_2_1_27_1","unstructured":"Ghilardi S. Nicolini E. and Zucchelli D. 2005. A comprehensive framework for combined decision procedures. Rapporto Interno DSI 304-05 Universit\u00e0 degli Studi di Milano Milano (Italy). (Available at http:\/\/homes.dsi.unimi.it\/~zucchell\/publications\/techreport\/GhiNiZu-RI304-05.pdf.)  Ghilardi S. Nicolini E. and Zucchelli D. 2005. A comprehensive framework for combined decision procedures. Rapporto Interno DSI 304-05 Universit\u00e0 degli Studi di Milano Milano (Italy). (Available at http:\/\/homes.dsi.unimi.it\/~zucchell\/publications\/techreport\/GhiNiZu-RI304-05.pdf.)"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2003)","volume":"2850","author":"Ghilardi S.","unstructured":"Ghilardi , S. and Santocanale , L . 2003. Algebraic and model theoretic techniques for fusion decidability in modal logics . In Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2003) (Almaty, Kazakhstan). Lecture Notes in Computer Science , vol. 2850 . Springer-Verlag, New York, 152--166. Ghilardi, S. and Santocanale, L. 2003. Algebraic and model theoretic techniques for fusion decidability in modal logics. In Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2003) (Almaty, Kazakhstan). Lecture Notes in Computer Science, vol. 2850. Springer-Verlag, New York, 152--166."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753628"},{"key":"e_1_2_1_30_1","volume-title":"Studies in Logic and the Foundations of Mathematics","volume":"147","author":"Hirsch R.","unstructured":"Hirsch , R. and Hodkinson , I . 2002. Relation Algebras by Games . Studies in Logic and the Foundations of Mathematics , vol. 147 . North-Holland Publishing Co., Amsterdam, Holland. Hirsch, R. and Hodkinson, I. 2002. Relation Algebras by Games. Studies in Logic and the Foundations of Mathematics, vol. 147. North-Holland Publishing Co., Amsterdam, Holland."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2004.02.002"},{"key":"e_1_2_1_33_1","volume-title":"Cambridge Studies in Advanced Mathematics","volume":"7","author":"Lambek J.","year":"1986","unstructured":"Lambek , J. and Scott , P. J . 1988. Introduction to Higher Order Categorical Logic . Cambridge Studies in Advanced Mathematics , vol. 7 . Cambridge University Press, Cambridge, UK. (Reprint of the 1986 original.) Lambek, J. and Scott, P. J. 1988. Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics, vol. 7. Cambridge University Press, Cambridge, UK. (Reprint of the 1986 original.)"},{"key":"e_1_2_1_34_1","unstructured":"MacLane S. and Birckhoff G. 1988. Algebra 3rd ed. Chelsea Publishing Co. New York.  MacLane S. and Birckhoff G. 1988. Algebra 3rd ed. Chelsea Publishing Co. New York."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011207512025"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2004)","volume":"3452","author":"Nieuwenhuis R.","unstructured":"Nieuwenhuis , R. , Oliveras , A. , and Tinelli , C . 2005. Abstract DPLL and abstract DPLL modulo theories . In Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2004) (Montevideo, Uruguay). Lecture Notes in Computer Science , vol. 3452 . Springer-Verlag, New York, 36--50. Nieuwenhuis, R., Oliveras, A., and Tinelli, C. 2005. Abstract DPLL and abstract DPLL modulo theories. In Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2004) (Montevideo, Uruguay). Lecture Notes in Computer Science, vol. 3452. Springer-Verlag, New York, 36--50."},{"volume-title":"Classical Recursion Theory. Studies in Logic and the Foundations of Mathematics","author":"Odifreddi P.","key":"e_1_2_1_39_1","unstructured":"Odifreddi , P. 1989. Classical Recursion Theory. Studies in Logic and the Foundations of Mathematics , vol. 125 . North-Holland Publishing Co. , Amsterdam, Holland . Odifreddi, P. 1989. Classical Recursion Theory. Studies in Logic and the Foundations of Mathematics, vol. 125. North-Holland Publishing Co., Amsterdam, Holland."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90059-6"},{"key":"e_1_2_1_41_1","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin M. O.","year":"1969","unstructured":"Rabin , M. O. 1969 . Decidability of second-order theories and automata on infinite trees . Trans. AMS 141 , 1 -- 35 . Rabin, M. O. 1969. Decidability of second-order theories and automata on infinite trees. Trans. AMS 141, 1--35.","journal-title":"Trans. AMS"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/646333.687633"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022587501759"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-009-0349-4_5"},{"key":"e_1_2_1_45_1","unstructured":"van Benthem J. 1985. Modal logic and classical logic. Monographs in Philosophical Logic and Formal Linguistics. Bibliopolis Naples Italy.  van Benthem J. 1985. Modal logic and classical logic. Monographs in Philosophical Logic and Formal Linguistics. Bibliopolis Naples Italy."},{"volume-title":"Proceedings of the Advances in Modal Logic","author":"Wolter F.","key":"e_1_2_1_46_1","unstructured":"Wolter , F. 1998. Fusions of modal logics revisited . In Proceedings of the Advances in Modal Logic , M. Kracht, M. de Rijke, H. Wansing, and M. Zakharyaschev, Eds. CSLI Lecture Notes, vol. 87 . CSLI Publisher , Stanford, CA, 361--379. Wolter, F. 1998. Fusions of modal logics revisited. In Proceedings of the Advances in Modal Logic, M. Kracht, M. de Rijke, H. Wansing, and M. Zakharyaschev, Eds. CSLI Lecture Notes, vol. 87. CSLI Publisher, Stanford, CA, 361--379."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.2307\/2695115"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1342991.1342992","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1342991.1342992","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:39:03Z","timestamp":1750253943000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1342991.1342992"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3]]},"references-count":46,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,3]]}},"alternative-id":["10.1145\/1342991.1342992"],"URL":"https:\/\/doi.org\/10.1145\/1342991.1342992","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2008,3]]},"assertion":[{"value":"2006-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2006-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-04-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}