{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:36:17Z","timestamp":1725550577542},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540290513"},{"type":"electronic","value":"9783540317302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11559306_1","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T12:50:36Z","timestamp":1127825436000},"page":"1-30","source":"Crossref","is-referenced-by-count":4,"title":["A Comprehensive Framework for Combined Decision Procedures"],"prefix":"10.1007","author":[{"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[]},{"given":"Enrica","family":"Nicolini","sequence":"additional","affiliation":[]},{"given":"Daniele","family":"Zucchelli","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1023\/A:1004275029985","volume":"27","author":"H. Andr\u00e9ka","year":"1998","unstructured":"Andr\u00e9ka, H., Nemeti, I., VanBenthem, J.: Modal languages and bounded fragments of predicate logics. Journal of Philosophical Logic\u00a027, 217\u2013274 (1998)","journal-title":"Journal of Philosophical Logic"},{"key":"1_CR2","series-title":"Applied Logic Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-9934-4","volume-title":"An introduction to mathematical logic and type theory: to truth through proof","author":"P.B. Andrews","year":"2002","unstructured":"Andrews, P.B.: An introduction to mathematical logic and type theory: to truth through proof. Applied Logic Series, vol.\u00a027. Kluwer Acad. Publ., Dordrecht (2002)"},{"key":"1_CR3","first-page":"966","volume-title":"Handbook of Automated Reasoning","author":"P.B. Andrews","year":"2001","unstructured":"Andrews, P.B.: Classical type theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0II, pp. 966\u20131007. Elsevier\/MIT, Cambridge (2001)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/11532231_21","volume-title":"Automated Deduction \u2013 CADE-20","author":"F. Baader","year":"2005","unstructured":"Baader, F., Ghilardi, S.: Connecting many-sorted theories. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol.\u00a03632, pp. 278\u2013294. Springer, Heidelberg (2005)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11559306_2","volume-title":"Frontiers of Combining Systems","author":"F. Baader","year":"2005","unstructured":"Baader, F., Ghilardi, S.: Connecting many-sorted structures and theories through adjoint functions. In: Gramlich, B. (ed.) FroCos 2005. LNCS, vol.\u00a03717, pp. 31\u201347. Springer, Heidelberg (2005)"},{"key":"1_CR6","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139172752","volume-title":"Term rewriting and all that","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, Cambridge (1998)"},{"issue":"2","key":"1_CR7","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":"1_CR8","unstructured":"Baader, F., Ghilardi, S., Tinelli, C.: A new combination procedure for the word problem that generalizes fusion decidability results in modal logics. Information and Computation (to appear)"},{"key":"1_CR9","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":"1_CR10","series-title":"Universitext","volume-title":"The classical decision problem","author":"E. B\u00f6rger","year":"2001","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The classical decision problem. Universitext. Springer, Berlin (2001)"},{"key":"1_CR11","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":"1_CR12","doi-asserted-by":"publisher","first-page":"1009","DOI":"10.1016\/B978-044450813-3\/50018-7","volume-title":"Handbook of Automated Reasoning","author":"G. Dowek","year":"2001","unstructured":"Dowek, G.: Higher order unification and matching. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0II, pp. 1009\u20131062. Elsevier\/MIT, Cambridge (2001)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-56732-1","volume-title":"Resolution Methods for the Decision Problem","author":"C. Ferm\u00fcller","year":"1993","unstructured":"Ferm\u00fcller, C., Tammet, T., Leitsch, A., Zamov, N.: Resolution Methods for the Decision Problem. LNCS, vol.\u00a0679. Springer, Heidelberg (1993)"},{"key":"1_CR14","doi-asserted-by":"publisher","first-page":"800","DOI":"10.2307\/2275098","volume":"58","author":"D.M. Gabbay","year":"1993","unstructured":"Gabbay, D.M., Shehtman, V.B.: Undecidability of modal and intermediate first-order logics with two individual variables. Journal of Symbolic Logic\u00a058, 800\u2013823 (1993)","journal-title":"Journal of Symbolic Logic"},{"key":"1_CR15","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Many-Dimensional Modal Logics: Theory and Applications","author":"D.M. Gabbay","year":"2003","unstructured":"Gabbay, D.M., Kurucz, A., Wolter, F., Zakharyaschev, M.: Many-Dimensional Modal Logics: Theory and Applications. Studies in Logic and the Foundations of Mathematics, vol.\u00a0148. Elsevier, Amsterdam (2003)"},{"issue":"3-3","key":"1_CR16","first-page":"221","volume":"33","author":"S. Ghilardi","year":"2005","unstructured":"Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. Journal of Automated Reasoning\u00a033(3-3), 221\u2013249 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR17","unstructured":"Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive framework for combined decision procedures. Technical Report 304-05, Dipartimento di Scienze dellInformazione, Universit\u00e0 degli Studi di Milano (2005), http:\/\/homes.dsi.unimi.it\/~ghilardi\/allegati\/frocos05.zip"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-48660-7_3","volume-title":"Automated Deduction - CADE-16","author":"E. Gr\u00e4del","year":"1999","unstructured":"Gr\u00e4del, E.: Decision procedures for guarded logics. In: Ganzinger, H. (ed.) CADE 1999. LNCS, vol.\u00a01632, pp. 31\u201351. Springer, Heidelberg (1999)"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Kontchakov, R., Kurucz, A., Zakharyaschev, M.: Undecidability of first-order intuituionistic and modal logics with two variables (2004) (manuscript)","DOI":"10.2178\/bsl\/1122038996"},{"key":"1_CR20","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1002\/malq.19620080204","volume":"8","author":"S. Kripke","year":"1962","unstructured":"Kripke, S.: The undecidability of monadic modal quantificational theory. Z. Math. Logik Grundlag. Math.\u00a08, 113\u2013116 (1962)","journal-title":"Z. Math. Logik Grundlag. Math."},{"key":"1_CR21","unstructured":"Lambek, J., Scott, P.J.: Introduction to higher order categorical logic. Cambridge Studies in Advanced Mathematics, vol.\u00a07"},{"key":"1_CR22","first-page":"228","volume":"76","author":"L. L\u00f6whenheim","year":"1915","unstructured":"L\u00f6whenheim, L.: \u00dcber M\u00f6glichkeiten im Relativkalk\u00fcl. Math. Annalen\u00a076, 228\u2013251 (1915)","journal-title":"Math. Annalen"},{"key":"1_CR23","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1023\/A:1011207512025","volume":"10","author":"M. Marx","year":"2001","unstructured":"Marx, M.: Tolerance logic. Journal of Logic, Language and Information\u00a010, 353\u2013374 (2001)","journal-title":"Journal of Logic, Language and Information"},{"key":"1_CR24","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1002\/malq.19750210118","volume":"21","author":"M. Mortimer","year":"1975","unstructured":"Mortimer, M.: On languages with two variables. Z. Math. Logik Grundlag. Math.\u00a021, 135\u2013140 (1975)","journal-title":"Z. Math. Logik Grundlag. Math."},{"issue":"2","key":"1_CR25","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":"1_CR26","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":"1_CR27","first-page":"477","volume":"27","author":"D. Scott","year":"1962","unstructured":"Scott, D.: A decision method for for validity of sentences in two variables. Journal of Symbolic Logic\u00a027, 477 (1962)","journal-title":"Journal of Symbolic Logic"},{"key":"1_CR28","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF02115610","volume":"2","author":"K. Segerberg","year":"1973","unstructured":"Segerberg, K.: Two-dimensional modal logic. Journal of Philosophical Logic\u00a02, 77\u201396 (1973)","journal-title":"Journal of Philosophical Logic"},{"key":"1_CR29","unstructured":"Shehtman, V.B.: On some two-dimensional modal logics. In: 8th Congress on Logic Methodology and Philosophy of Science, Nauka, Moskow, vol.\u00a01, pp. 326\u2013330 (1987)"},{"issue":"1","key":"1_CR30","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"},{"key":"1_CR31","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-94-009-0349-4_5","volume-title":"Proc. of the 1st Int. Workshop on Frontiers of Combining Systems","author":"C. Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson\u2013Oppen combination procedure. In: Proc. of the 1st Int. Workshop on Frontiers of Combining Systems, pp. 103\u2013120. Kluwer Acad. Publ., Dordrecht (1996)"},{"key":"1_CR32","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.2307\/2695115","volume":"66","author":"F. Wolter","year":"2001","unstructured":"Wolter, F., Zakharyaschev, M.: Decidable fragments of first-order modal logics. Journal of Symbolic Logic\u00a066, 1415\u20131438 (2001)","journal-title":"Journal of Symbolic Logic"},{"key":"1_CR33","volume-title":"Advances in Modal Logic","author":"F. Wolter","year":"1998","unstructured":"Wolter, F.: Fusions of modal logics revisited. In: Kracht, M., de Rijke, M., Wansing, H., Zakharyaschev, M. (eds.) Advances in Modal Logic. CSLI, Stanford (1998)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11559306_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:49:19Z","timestamp":1605642559000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11559306_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540290513","9783540317302"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/11559306_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}