{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,23]],"date-time":"2025-12-23T15:43:27Z","timestamp":1766504607665},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642042218"},{"type":"electronic","value":"9783642042225"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04222-5_16","type":"book-chapter","created":{"date-parts":[[2009,9,16]],"date-time":"2009-09-16T12:42:11Z","timestamp":1253104931000},"page":"263-278","source":"Crossref","is-referenced-by-count":20,"title":["Combinations of Theories for Decidable Fragments of First-Order Logic"],"prefix":"10.1007","author":[{"given":"Pascal","family":"Fontaine","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)"},{"key":"16_CR2","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/B978-044450813-3\/50007-2","volume-title":"Handbook of Automated Reasoning, ch. 5","author":"M. Baaz","year":"2001","unstructured":"Baaz, M., Egly, U., Leitsch, A.: Normal form transformations. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 5, vol.\u00a0I, pp. 273\u2013333. Elsevier Science B.V, Amsterdam (2001)"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the Model Evolution Calculus. In: Schulz, S., Sutcliffe, G., Tammet, T. (eds.) Special Issue of the International Journal of Artificial Intelligence Tools (IJAIT). International Journal of Artificial Intelligence Tools, vol.\u00a015 (2005)","DOI":"10.1142\/S0218213006002552"},{"key":"16_CR4","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/BF01459101","volume":"99","author":"P. Bernays","year":"1928","unstructured":"Bernays, P., Sch\u00f6nfinkel, M.: Zum Entscheidungsproblem der mathematischen Logik. Math. Annalen\u00a099, 342\u2013372 (1928)","journal-title":"Math. Annalen"},{"key":"16_CR5","series-title":"Perspectives in Mathematical Logic","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem","author":"E. B\u00f6rger","year":"1997","unstructured":"B\u00f6rger, E., Gr\u00e4del, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, Berlin (1997)"},{"key":"16_CR6","volume-title":"The Decision Problem: Solvable Classes of Quantificational Formulas","author":"B. Dreben","year":"1979","unstructured":"Dreben, B., Goldfarb, W.D.: The Decision Problem: Solvable Classes of Quantificational Formulas. Addison-Wesley, Reading (1979)"},{"key":"16_CR7","series-title":"Perspectives in Mathematical Logic","volume-title":"Finite Model Theory","author":"H.-D. Ebbinghaus","year":"1995","unstructured":"Ebbinghaus, H.-D., Flum, J.: Finite Model Theory. Perspectives in Mathematical Logic. Springer, Berlin (1995)"},{"key":"16_CR8","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"1972","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic, Orlando, Florida. Academic Press Inc., London (1972)"},{"key":"16_CR9","unstructured":"Fontaine, P.: Combinations of theories and the Bernays-Sch\u00f6nfinkel-Ramsey class. In: Beckert, B. (ed.) 4th International Verification Workshop - VERIFY 2007, Bremen (15\/07\/07-16\/07\/07) (July 2007)"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Fontaine, P.: Combinations of theories for decidable fragments of first-order logic (2009), http:\/\/www.loria.fr\/~fontaine\/Fontaine12b.pdf","DOI":"10.1007\/978-3-642-04222-5_16"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-36577-X_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Fontaine","year":"2003","unstructured":"Fontaine, P., Gribomont, E.P.: Decidability of invariant validation for parameterized systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 97\u2013112. Springer, Heidelberg (2003)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Fontaine, P., Gribomont, E.P.: Combining non-stably infinite, non-first order theories. In: Ahrendt, W., Baumgartner, P., de Nivelle, H., Ranise, S., Tinelli, C. (eds.) Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR 2004), July 2005. Electronic Notes in Theoretical Computer Science, vol.\u00a0125, pp. 37\u201351 (2005)","DOI":"10.1016\/j.entcs.2004.06.066"},{"issue":"1","key":"16_CR13","doi-asserted-by":"publisher","first-page":"53","DOI":"10.2307\/421196","volume":"3","author":"E. Gr\u00e4del","year":"1997","unstructured":"Gr\u00e4del, E., Kolaitis, P.G., Vardi, M.Y.: On the decision problem for two-variable first-order logic. The Bulletin of Symbolic Logic\u00a03(1), 53\u201369 (1997)","journal-title":"The Bulletin of Symbolic Logic"},{"key":"16_CR14","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1109\/LICS.2003.1210069","volume-title":"LICS 2003: Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science","author":"Y. Gurevich","year":"2003","unstructured":"Gurevich, Y., Shelah, S.: Spectra of monadic second-order formulas with one unary function. In: LICS 2003: Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, pp. 291\u2013300. IEEE Computer Society, Washington (2003)"},{"key":"16_CR15","volume-title":"Specifying Systems","author":"L. Lamport","year":"2002","unstructured":"Lamport, L.: Specifying Systems. Addison-Wesley, Boston (2002)"},{"issue":"2","key":"16_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.: Simplifications by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR17","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1112\/plms\/s2-30.1.264","volume":"30","author":"F.P. Ramsey","year":"1930","unstructured":"Ramsey, F.P.: On a Problem of Formal Logic. Proceedings of the London Mathematical Society\u00a030, 264\u2013286 (1930)","journal-title":"Proceedings of the London Mathematical Society"},{"issue":"2","key":"16_CR18","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of Vampire. AI Communications\u00a015(2), 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"16_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/3-540-45744-5_28","volume-title":"Automated Reasoning","author":"S. Schulz","year":"2001","unstructured":"Schulz, S.: System Abstract: E 0.61. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 370\u2013375. Springer, Heidelberg (2001)"},{"issue":"1","key":"16_CR20","first-page":"35","volume":"19","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The State of CASC. AI Communications\u00a019(1), 35\u201348 (2006)","journal-title":"AI Communications"},{"key":"16_CR21","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-94-009-0349-4_5","volume-title":"Frontiers of Combining Systems (FroCoS), Applied Logic","author":"C. Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson\u2013Oppen combination procedure. In: Baader, F., Schulz, K.U. (eds.) Frontiers of Combining Systems (FroCoS), Applied Logic, pp. 103\u2013120. Kluwer Academic Publishers, Dordrecht (1996)"},{"issue":"1","key":"16_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"},{"issue":"3","key":"16_CR23","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C. Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.G.: Combining non-stably infinite theories. Journal of Automated Reasoning\u00a034(3), 209\u2013238 (2005)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR24","series-title":"LNAI","first-page":"366","volume-title":"FroCoS 2009","author":"T. Wies","year":"2009","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol.\u00a05749, pp. 366\u2013382. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04222-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T13:17:48Z","timestamp":1558531068000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04222-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642042218","9783642042225"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04222-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}