{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,10]],"date-time":"2026-11-10T22:14:53Z","timestamp":1794348893523,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540746201","type":"print"},{"value":"9783540746218","type":"electronic"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-74621-8_14","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T07:46:32Z","timestamp":1187768792000},"page":"206-220","source":"Crossref","is-referenced-by-count":3,"title":["Noetherianity and Combination Problems"],"prefix":"10.1007","author":[{"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Enrica","family":"Nicolini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniele","family":"Zucchelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Artificial Intelligence","first-page":"65","volume-title":"FroCoS 2005","author":"A. Armando","year":"2005","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a rewriting approach to satisfiability procedures: extension, combination of theories and an experimental appraisal. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol.\u00a03717, pp. 65\u201380. Springer, Heidelberg (2005)"},{"key":"14_CR2","first-page":"1","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 A.I. Research\u00a016, 1\u201358 (2002)","journal-title":"Journal of A.I. Research"},{"key":"14_CR3","unstructured":"Baumgartner, P., Furbach, U., Petermann, U.: A unified approach to theory reasoning. Research Report 15\u201392, Universit\u00e4t Koblenz-Landau (1992)"},{"key":"14_CR4","volume-title":"Modal Logic","author":"P. Blackburn","year":"2002","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2002)"},{"key":"14_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/11814771_42","volume-title":"Automated Reasoning","author":"M.P. Bonacina","year":"2006","unstructured":"Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 513\u2013527. Springer, Heidelberg (2006)"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 78\u201392. Springer, Heidelberg (2002)"},{"key":"14_CR7","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70075-2","volume-title":"Model Theory","author":"C.-C. Chang","year":"1990","unstructured":"Chang, C.-C., Keisler, J.H.: Model Theory, 3rd edn. North-Holland, Amsterdam-London (1990)","edition":"3"},{"key":"14_CR8","unstructured":"Le Chenadec, P.: Canonical Forms in Finitely Presented Algebras. Research Notes in Theoretical Computer Science. Pitman-Wiley (1986)"},{"issue":"1","key":"14_CR9","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1145\/1119439.1119443","volume":"7","author":"A. Degtyarev","year":"2006","unstructured":"Degtyarev, A., Fisher, M., Konev, B.: Monodic temporal resolution. ACM Transaction on Computational Logic\u00a07(1), 108\u2013150 (2006)","journal-title":"ACM Transaction on Computational Logic"},{"key":"14_CR10","volume-title":"Undergraduate Texts in Mathematics","author":"H.-D. Ebbinghaus","year":"1994","unstructured":"Ebbinghaus, H.-D., Flum, J., Thomas, W.: Mathematical logic. In: Undergraduate Texts in Mathematics, 2nd edn., Springer, Heidelberg (1994)","edition":"2"},{"issue":"3","key":"14_CR11","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/BF00156915","volume":"1","author":"M. Finger","year":"1992","unstructured":"Finger, M., Gabbay, D.M.: Adding a temporal dimension to a logic system. Journal of Logic, Language, and Information\u00a01(3), 203\u2013233 (1992)","journal-title":"Journal of Logic, Language, and Information"},{"key":"14_CR12","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. North-Holland, Amsterdam (2003)"},{"issue":"3-4","key":"14_CR13","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-4), 221\u2013249 (2004)","journal-title":"Journal of Automated Reasoning"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1007\/978-3-540-73595-3_25","volume-title":"CADE 2007","author":"S. Ghilardi","year":"2007","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Combination methods for satisfiability and model-checking of infinite-state systems. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol.\u00a04603, pp. 362\u2013378. Springer, Heidelberg (2007)"},{"key":"14_CR15","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Combination methods for satisfiability and model-checking of infinite-state systems. Technical Report RI313-07, Universit\u00e0 degli Studi di Milano (2007) Available at \n                    \n                      http:\/\/homes.dsi.unimi.it\/~zucchell\/publications\/techreport\/GhiNiRaZu-RI313-07.pdf"},{"key":"14_CR16","unstructured":"Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive framework for combined decision procedures. ACM Transactions on Computational Logic (to appear)"},{"issue":"1\u20133","key":"14_CR17","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/S0168-0072(00)00018-X","volume":"106","author":"I.M. Hodkinson","year":"2000","unstructured":"Hodkinson, I.M., Wolter, F., Zakharyaschev, M.: Decidable fragment of first-order temporal logics. Annals of Pure and Applied Logic\u00a0106(1\u20133), 85\u2013134 (2000)","journal-title":"Annals of Pure and Applied Logic"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1007\/11560647_39","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2005","author":"H. Kirchner","year":"2005","unstructured":"Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: On superposition-based satisfiability procedures and their combination. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol.\u00a03722, pp. 594\u2013608. Springer, Heidelberg (2005)"},{"issue":"3","key":"14_CR19","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Transactions on Programming Languages and Systems\u00a016(3), 872\u2013923 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"14_CR20","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/BF00245296","volume":"9","author":"J.-L. Lassez","year":"1992","unstructured":"Lassez, J.-L., Maher, M.J.: On Fourier\u2019s algorithm for linear arithmetic constraints. Journal of Automated Reasoning\u00a09(3), 373\u2013379 (1992)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"14_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0747-7171(92)90002-L","volume":"13","author":"J.-L. Lassez","year":"1992","unstructured":"Lassez, J.-L., McAloon, K.: A canonical form for generalized linear constraints. Journal of Symbolic Computation\u00a013(1), 1\u201324 (1992)","journal-title":"Journal of Symbolic Computation"},{"key":"14_CR22","volume-title":"Algebra","author":"S. MacLane","year":"1988","unstructured":"MacLane, S., Birkhoff, G.: Algebra, 3rd edn. Chelsea Publishing, New York (USA) (1988)","edition":"3"},{"key":"14_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)"},{"key":"14_CR24","unstructured":"Merz, S.: Isabelle\/TLA (1999), Available at \n                    \n                      http:\/\/isabelle.in.tum.de\/library\/HOL\/TLA"},{"key":"14_CR25","first-page":"351","volume":"22","author":"S. Merz","year":"2003","unstructured":"Merz, S.: On the logic of TLA. Computing and Informatics\u00a022, 351\u2013379 (2003)","journal-title":"Computing and Informatics"},{"issue":"3","key":"14_CR26","doi-asserted-by":"publisher","first-page":"437","DOI":"10.2307\/1970290","volume":"74","author":"M.L. Minsky","year":"1961","unstructured":"Minsky, M.L.: Recursive unsolvability of Post\u2019s problem of \u201ctag\u201d and other topics in the theory of Turing machines. Annals of Mathematics\u00a074(3), 437\u2013455 (1961)","journal-title":"Annals of Mathematics"},{"issue":"2","key":"14_CR27","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 Transaction on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"14_CR28","unstructured":"Nicolini, E.: Combined decision procedures for constraint satisfiability. PhD thesis, Dipartimento di Matematica, Universit\u00e0 degli Studi di Milano (2007)"},{"issue":"2","key":"14_CR29","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/BF02432150","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A.: A decision procedure for combination of propositional temporal logic and other specialized theories. Journal of Automated Reasoning\u00a02(2), 171\u2013190 (1986)","journal-title":"Journal of Automated Reasoning"},{"issue":"6","key":"14_CR30","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1109\/MIS.2006.117","volume":"21","author":"S. Ranise","year":"2006","unstructured":"Ranise, S., Tinelli, C.: Satisfiability modulo theories. IEEE Magazine on Intelligent Systems\u00a021(6), 71\u201381 (2006)","journal-title":"IEEE Magazine on Intelligent Systems"},{"key":"14_CR31","first-page":"103","volume-title":"Proc. of FroCoS 1996, Applied Logic","author":"C. Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Proc. of FroCoS 1996, Applied Logic, pp. 103\u2013120. Kluwer Academic Publishers, Dordrecht (1996)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74621-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T10:09:15Z","timestamp":1558260555000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74621-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540746201","9783540746218"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74621-8_14","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-540-74621-8","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007]]}}}