{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:35:19Z","timestamp":1740123319346,"version":"3.37.3"},"reference-count":148,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2020,7,18]],"date-time":"2020-07-18T00:00:00Z","timestamp":1595030400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,7,18]],"date-time":"2020-07-18T00:00:00Z","timestamp":1595030400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100004189","name":"Max-Planck-Gesellschaft","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004189","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2021,3]]},"DOI":"10.1007\/s10817-020-09567-8","type":"journal-article","created":{"date-parts":[[2020,7,18]],"date-time":"2020-07-18T11:02:48Z","timestamp":1595070168000},"page":"357-423","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Decidable $${\\exists }^*{\\forall }^*$$ First-Order Fragments of Linear Rational Arithmetic with Uninterpreted Predicates"],"prefix":"10.1007","volume":"65","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5666-7125","authenticated-orcid":false,"given":"Marco","family":"Voigt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,18]]},"reference":[{"issue":"2","key":"9567_CR1","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1016\/j.jsc.2009.03.003","volume":"45","author":"A Abadi","year":"2010","unstructured":"Abadi, A., Rabinovich, A., Sagiv, M.: Decidable fragments of many-sorted logic. J. Symb. Comput. 45(2), 153\u2013172 (2010)","journal-title":"J. Symb. Comput."},{"key":"9567_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, A., Rabinovich, A.M., Sagiv, M.: Decidable fragments of many-sorted logic. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201907), pp. 17\u201331 (2007)","DOI":"10.1007\/978-3-540-75560-9_4"},{"key":"9567_CR3","doi-asserted-by":"crossref","unstructured":"Alagi, G., Weidenbach, C.: NRCL\u2014a model building approach to the Bernays\u2013Sch\u00f6nfinkel fragment. In: Frontiers of Combining Systems (FroCoS\u201915), LNCS 9322, pp. 69\u201384. Springer (2015)","DOI":"10.1007\/978-3-319-24246-0_5"},{"key":"9567_CR4","doi-asserted-by":"crossref","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Frontiers of Combining Systems (FroCoS\u201909), pp. 84\u201399 (2009)","DOI":"10.1007\/978-3-642-04222-5_5"},{"key":"9567_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: Automata for modeling real-time systems. In: Automata, Languages and Programming (ICALP\u201990), pp. 322\u2013335 (1990)","DOI":"10.1007\/BFb0032042"},{"issue":"2","key":"9567_CR6","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"9567_CR7","doi-asserted-by":"crossref","unstructured":"Areces, C., Fontaine, P.: Combining theories: the Ackerman and guarded fragments. In: Frontiers of Combining Systems (FroCoS\u201911), pp. 40\u201354 (2011)","DOI":"10.1007\/978-3-642-24364-6_4"},{"issue":"1","key":"9567_CR8","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/1459010.1459014","volume":"10","author":"A Armando","year":"2009","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log. 10(1), 129\u2013179 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"9567_CR9","doi-asserted-by":"crossref","unstructured":"Armando, A., Castellini, C., Giunchiglia, E., Maratea, M.: A SAT-based decision procedure for the Boolean combination of difference constraints. In: Theory and Applications of Satisfiability Testing (SAT\u201904), Revised Selected Papers (2004)","DOI":"10.1007\/11527695_2"},{"key":"9567_CR10","doi-asserted-by":"crossref","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Theorem proving for hierarchic first-order theories. In: Algebraic and Logic Programming (ALP\u201992), pp. 420\u2013434 (1992)","DOI":"10.1007\/BFb0013841"},{"key":"9567_CR11","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/BF01190829","volume":"5","author":"L Bachmair","year":"1994","unstructured":"Bachmair, L., Ganzinger, H., Waldmann, U.: Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput. 5, 193\u2013212 (1994)","journal-title":"Appl. Algebra Eng. Commun. Comput."},{"key":"9567_CR12","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"9567_CR13","unstructured":"Barbosa, H.: New techniques for instantiation and proof production in SMT solving (nouvelles techniques pour l\u2019instanciation et la production des preuves dans SMT). Ph.D. thesis, University of Lorraine, Nancy, France (2017)"},{"key":"9567_CR14","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"C Barrett","year":"2018","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305\u2013343. Springer, Berlin (2018)"},{"issue":"1","key":"9567_CR15","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1016\/j.jal.2007.07.005","volume":"7","author":"P Baumgartner","year":"2009","unstructured":"Baumgartner, P., Fuchs, A., de Nivelle, H., Tinelli, C.: Computing finite models by reduction to function-free clause logic. J. Appl. Log. 7(1), 58\u201374 (2009)","journal-title":"J. Appl. Log."},{"key":"9567_CR16","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition: completeness without compactness. In: Ko\u0161ta, M., Sturm, T. (eds.) Fifth International Conference on Mathematical Aspects of Computer and Information Sciences (MACIS\u201913), pp. 8\u201312 (2013)"},{"key":"9567_CR17","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Automated Deduction (CADE-24), LNCS 7898, pp. 39\u201357. Springer (2013)","DOI":"10.1007\/978-3-642-38574-2_3"},{"key":"9567_CR18","unstructured":"Blumensath, A., Gr\u00e4del, E.: Automatic structures. In: Logic in Computer Science (LICS 2000), pp. 51\u201362 (2000)"},{"issue":"6","key":"9567_CR19","doi-asserted-by":"crossref","first-page":"641","DOI":"10.1007\/s00224-004-1133-y","volume":"37","author":"A Blumensath","year":"2004","unstructured":"Blumensath, A., Gr\u00e4del, E.: Finite presentations of infinite structures: automata and interpretations. Theory Comput. Syst. 37(6), 641\u2013674 (2004)","journal-title":"Theory Comput. Syst."},{"key":"9567_CR20","doi-asserted-by":"crossref","unstructured":"Bonacina, M.P., Fontaine, P., Ringeissen, C., Tinelli, C.: Theory combination: beyond equality sharing. In: Description Logic, Theory Combination, and All That\u2014Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, pp. 57\u201389 (2019)","DOI":"10.1007\/978-3-030-22102-7_3"},{"key":"9567_CR21","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59207-2","volume-title":"The Classical Decision Problem. Perspectives in Mathematical Logic","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":"9567_CR22","doi-asserted-by":"crossref","first-page":"1001","DOI":"10.1007\/978-3-319-10575-8_29","volume-title":"Handbook of Model Checking","author":"P Bouyer","year":"2018","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Ouaknine, J., Worrell, J.: Model checking real-time systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 1001\u20131046. Springer, Berlin (2018)"},{"key":"9567_CR23","unstructured":"Bradley, A.R.: Safety analysis of systems. Ph.D. thesis, Department of Computer Science of Stanford University (2007)"},{"key":"9567_CR24","series-title":"Texts in Theoretical Computer Science. An EATCS Series","volume-title":"The Calculus of Computation\u2014Decision Procedures with Applications to Verification","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation\u2014Decision Procedures with Applications to Verification. Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin (2007)"},{"key":"9567_CR25","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Verification, Model Checking, and Abstract Interpretation (VMCAI\u201906), pp. 427\u2013442 (2006)","DOI":"10.1007\/11609773_28"},{"issue":"1\u20133","key":"9567_CR26","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1007\/s10472-013-9337-y","volume":"71","author":"D Bresolin","year":"2014","unstructured":"Bresolin, D., Della Monica, D., Montanari, A., Sciavicco, G.: The light side of interval temporal logic: the Bernays\u2013Sch\u00f6nfinkel fragment of CDT. Ann. Math. Artif. Intell. 71(1\u20133), 11\u201339 (2014)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9567_CR27","doi-asserted-by":"crossref","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: Computer Aided Verification (CAV\u201902), pp. 78\u201392 (2002)","DOI":"10.1007\/3-540-45657-0_7"},{"key":"9567_CR28","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1002\/malq.19600060105","volume":"6","author":"JR B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R.: Weak second-order arithmetic and finite automata. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik 6, 66\u201392 (1960)","journal-title":"Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik"},{"key":"9567_CR29","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Nagel, E., Suppes, P., Tarski, A. (eds.) Proceedings of the 1960 International Congress on Logic, Methodology and Philosophy of Science, pp. 1\u201311. Stanford University Press (1962)"},{"key":"9567_CR30","doi-asserted-by":"crossref","unstructured":"Charatonik, W., Witkowski, P.: On the complexity of the Bernays\u2013Sch\u00f6nfinkel class with datalog. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), LNCS 6397, pp. 187\u2013201. Springer (2010)","DOI":"10.1007\/978-3-642-16242-8_14"},{"key":"9567_CR31","doi-asserted-by":"crossref","unstructured":"Chocron, P., Fontaine, P., Ringeissen, C.: A gentle non-disjoint combination of satisfiability procedures. In: Automated Reasoning (IJCAR\u201914), pp. 122\u2013136 (2014)","DOI":"10.1007\/978-3-319-08587-6_9"},{"key":"9567_CR32","doi-asserted-by":"crossref","unstructured":"Chocron, P., Fontaine, P., Ringeissen, C.: A polite non-disjoint combination method: theories with bridging functions revisited. In: Automated Deduction (CADE-25), pp. 419\u2013433 (2015)","DOI":"10.1007\/978-3-319-21401-6_29"},{"key":"9567_CR33","doi-asserted-by":"crossref","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis and Presburger arithmetic. In: Computer Aided Verification (CAV\u201998), pp. 268\u2013279 (1998)","DOI":"10.1007\/BFb0028751"},{"key":"9567_CR34","doi-asserted-by":"crossref","unstructured":"Comon, H., Jurski, Y.: Timed automata and the theory of real numbers. In: Concurrency Theory (CONCUR\u201999), pp. 242\u2013257 (1999)","DOI":"10.1007\/3-540-48320-9_18"},{"issue":"2","key":"9567_CR35","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1016\/j.tcs.2005.11.025","volume":"354","author":"S Conchon","year":"2006","unstructured":"Conchon, S., Krstic, S.: Strategies for combining decision procedures. Theor. Comput. Sci. 354(2), 187\u2013210 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"9567_CR36","doi-asserted-by":"crossref","unstructured":"Cotton, S., Asarin, E., Maler, O., Niebert, P.: Some progress in satisfiability checking for difference logic. In: Formal Modelling and Analysis of Timed Systems and Formal Techniques in Real-Time and Fault-Tolerant Systems (FORMATS\/FTRTFT\u201904), pp. 263\u2013276 (2004)","DOI":"10.1007\/978-3-540-30206-3_19"},{"key":"9567_CR37","doi-asserted-by":"crossref","unstructured":"Cotton, S., Maler, O.: Fast and flexible difference constraint propagation for DPLL(T). In: Theory and Applications of Satisfiability Testing (SAT\u201906), pp. 170\u2013183 (2006)","DOI":"10.1007\/11814948_19"},{"key":"9567_CR38","first-page":"17","volume-title":"Constraint Logic Programming, Selected Research","author":"J Cox","year":"1993","unstructured":"Cox, J., McAloon, K.: Decision procedures for constraint-based extensions of Datalog. In: Benhamou, F., Colmerauer, A. (eds.) Constraint Logic Programming, Selected Research, pp. 17\u201332. The MIT Press, Cambridge (1993)"},{"issue":"2\u20134","key":"9567_CR39","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/BF01543475","volume":"5","author":"J Cox","year":"1992","unstructured":"Cox, J., McAloon, K., Tretkoff, C.: Computational complexity and constraint logic programming languages. Ann. Math. Artif. Intell. 5(2\u20134), 163\u2013189 (1992)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9567_CR40","unstructured":"Downey, P.J.: Undecidability of Presburger arithmetic with a single monadic predicate letter. Center for Research in Computer Technology, Harvard University, Technical report (1972)"},{"key":"9567_CR41","doi-asserted-by":"crossref","first-page":"1047","DOI":"10.1007\/978-3-319-10575-8_30","volume-title":"Handbook of Model Checking","author":"L Doyen","year":"2018","unstructured":"Doyen, L., Frehse, G., Pappas, G.J., Platzer, A.: Verification of hybrid systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 1047\u20131110. Springer, Berlin (2018)"},{"key":"9567_CR42","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-2355-7","volume-title":"Mathematical Logic","author":"H Ebbinghaus","year":"1994","unstructured":"Ebbinghaus, H., Flum, J., Thomas, W.: Mathematical Logic, 2nd edn. Springer, Berlin (1994)","edition":"2"},{"key":"9567_CR43","doi-asserted-by":"crossref","unstructured":"Eggers, A., Kruglov, E., Kupferschmid, S., Scheibler, K., Teige, T., Weidenbach, C.: Superposition modulo non-linear arithmetic. In: Frontiers of Combining Systems (FroCoS\u201911), pp. 119\u2013134 (2011)","DOI":"10.1007\/978-3-642-24364-6_9"},{"key":"9567_CR44","doi-asserted-by":"crossref","unstructured":"Emmer, M., Khasidashvili, Z., Korovin, K., Sticksel, C., Voronkov, A.: EPR-based bounded model checking at word level. In: Automated Reasoning (IJCAR\u201912), pp. 210\u2013224 (2012)","DOI":"10.1007\/978-3-642-31365-3_18"},{"key":"9567_CR45","unstructured":"Emmer, M., Khasidashvili, Z., Korovin, K., Voronkov, A.: Encoding industrial hardware verification problems into effectively propositional logic. In: Formal Methods in Computer-Aided Design (FMCAD\u201910), pp. 137\u2013144 (2010)"},{"key":"9567_CR46","volume-title":"A Mathematical Introduction to Logic","author":"HB Enderton","year":"1972","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, London (1972)"},{"key":"9567_CR47","doi-asserted-by":"crossref","first-page":"1791","DOI":"10.1016\/B978-044450813-3\/50027-8","volume-title":"Handbook of Automated Reasoning","author":"CG Ferm\u00fcller","year":"2001","unstructured":"Ferm\u00fcller, C.G., Leitsch, A., Hustadt, U., Tammet, T.: Resolution decision procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. II, pp. 1791\u20131849. Elsevier, Amsterdam (2001)"},{"key":"9567_CR48","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0062837","volume-title":"The Computational Complexity of Logical Theories","author":"J Ferrante","year":"1979","unstructured":"Ferrante, J., Rackoff, C.W.: The Computational Complexity of Logical Theories. Springer, Berlin (1979)"},{"key":"9567_CR49","unstructured":"Fietzke, A.: Labelled superposition. Ph.D. thesis, Department of Computer Science, Saarland University (2013)"},{"issue":"4","key":"9567_CR50","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/s11786-012-0134-5","volume":"6","author":"A Fietzke","year":"2012","unstructured":"Fietzke, A., Weidenbach, C.: Superposition as a decision procedure for timed automata. Math. Comput. Sci. 6(4), 409\u2013425 (2012)","journal-title":"Math. Comput. Sci."},{"key":"9567_CR51","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., M\u00fcller, C., Seidl, H., Zalinescu, E.: Verifying security policies in multi-agent workflows with loops. In: Computer and Communications Security (CCS\u201917), pp. 633\u2013645 (2017)","DOI":"10.1145\/3133956.3134080"},{"key":"9567_CR52","unstructured":"Fontaine, P.: Combinations of theories and the Bernays\u2013Sch\u00f6nfinkel\u2013Ramsey class. In: Verification Workshop in connection with CADE-21 (VERIFY\u201907) (2007)"},{"key":"9567_CR53","doi-asserted-by":"crossref","unstructured":"Fontaine, P.: Combinations of theories for decidable fragments of first-order logic. In: Frontiers of Combining Systems (FroCoS\u201909), LNCS 5749, pp. 263\u2013278. Springer (2009)","DOI":"10.1007\/978-3-642-04222-5_16"},{"key":"9567_CR54","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-05138-2","volume-title":"Essentials of Constraint Programming","author":"T Fr\u00fchwirth","year":"2003","unstructured":"Fr\u00fchwirth, T., Abdennadher, S.: Essentials of Constraint Programming. Springer, Berlin (2003)"},{"key":"9567_CR55","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/BFb0120921","volume":"14","author":"P G\u00e1cs","year":"1981","unstructured":"G\u00e1cs, P., Lov\u00e1sz, L.: Khachiyan\u2019s algorithm for linear programming. Math. Program. Study 14, 61\u201368 (1981)","journal-title":"Math. Program. Study"},{"key":"9567_CR56","doi-asserted-by":"crossref","unstructured":"Ganzinger, H.: Shostak light. In: Automated Deduction (CADE-18), pp. 332\u2013346 (2002)","DOI":"10.1007\/3-540-45620-1_28"},{"key":"9567_CR57","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): fast decision procedures. In: Computer Aided Verification (CAV\u201904), pp. 175\u2013188 (2004)","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"9567_CR58","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hillenbrand, T., Waldmann, U.: Superposition modulo a shostak theory. In: Automated Deduction (CADE-19), pp. 182\u2013196 (2003)","DOI":"10.1007\/978-3-540-45085-6_15"},{"key":"9567_CR59","doi-asserted-by":"crossref","unstructured":"Ge, Y., de\u00a0Moura, L.M.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Computer Aided Verification (CAV\u201909), LNCS 5643, pp. 306\u2013320. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_25"},{"issue":"8","key":"9567_CR60","doi-asserted-by":"crossref","first-page":"731","DOI":"10.1016\/j.apal.2018.04.001","volume":"169","author":"S Ghilardi","year":"2018","unstructured":"Ghilardi, S., Gianola, A.: Modularity results for interpolation, amalgamation and superamalgamation. Ann. Pure Appl. Log. 169(8), 731\u2013754 (2018)","journal-title":"Ann. Pure Appl. Log."},{"issue":"2","key":"9567_CR61","doi-asserted-by":"crossref","first-page":"8:1","DOI":"10.1145\/1342991.1342992","volume":"9","author":"S Ghilardi","year":"2008","unstructured":"Ghilardi, S., Nicolini, E., Zucchelli, D.: A comprehensive combination framework. ACM Trans. Comput. Log. 9(2), 8:1\u20138:54 (2008)","journal-title":"ACM Trans. Comput. Log."},{"key":"9567_CR62","volume-title":"Ramsey Theory. A Wiley-Interscience Publication","author":"R Graham","year":"1990","unstructured":"Graham, R., Rothschild, B., Spencer, J.: Ramsey Theory. A Wiley-Interscience Publication, 2nd edn. Wiley, Hoboken (1990)","edition":"2"},{"key":"9567_CR63","doi-asserted-by":"crossref","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: Foundations of Software Science and Computational Structures (FOSSACS\u201908), pp. 474\u2013489 (2008)","DOI":"10.1007\/978-3-540-78499-9_33"},{"issue":"2","key":"9567_CR64","doi-asserted-by":"crossref","first-page":"637","DOI":"10.2307\/2274706","volume":"56","author":"JY Halpern","year":"1991","unstructured":"Halpern, J.Y.: Presburger arithmetic with unary predicates is $$\\Pi ^1_1$$ complete. J. Symb. Log. 56(2), 637\u2013642 (1991)","journal-title":"J. Symb. Log."},{"issue":"2","key":"9567_CR65","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"TA Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193\u2013244 (1994)","journal-title":"Inf. Comput."},{"key":"9567_CR66","unstructured":"Hillenbrand, T.: Superposition and decision procedures back and forth. Ph.D. thesis, Department of Computer Science, Saarland University (2008)"},{"key":"9567_CR67","doi-asserted-by":"crossref","unstructured":"Hillenbrand, T., Weidenbach, C.: Superposition for bounded domains. In: Automated Reasoning and Mathematics\u2014Essays in Memory of William W. McCune, LNCS 7788, pp. 68\u2013100. Springer (2013)","DOI":"10.1007\/978-3-642-36675-8_4"},{"key":"9567_CR68","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1016\/j.artint.2012.06.001","volume":"194","author":"J Hoffart","year":"2013","unstructured":"Hoffart, J., Suchanek, F.M., Berberich, K., Weikum, G.: YAGO2: a spatially and temporally enhanced knowledge base from Wikipedia. Artif. Intell. 194, 28\u201361 (2013)","journal-title":"Artif. Intell."},{"key":"9567_CR69","doi-asserted-by":"crossref","unstructured":"Horbach, M., Voigt, M., Weidenbach, C.: On the combination of the Bernays\u2013Sch\u00f6nfinkel\u2013Ramsey fragment with simple linear integer arithmetic. In: Automated Deduction (CADE\u201917), LNCS 10395, pp. 77\u201394 (2017). An extended version is available at the arXiv\u00a0preprint server under the signature arXiv:1705.08792 [cs.LO]","DOI":"10.1007\/978-3-319-63046-5_6"},{"key":"9567_CR70","unstructured":"Horbach, M., Voigt, M., Weidenbach, C.: The universal fragment of Presburger arithmetic with unary uninterpreted predicates is undecidable. ArXiv preprint arXiv:1703.01212 [cs.LO] (2017)"},{"key":"9567_CR71","doi-asserted-by":"crossref","unstructured":"Ihlemann, C.: Reasoning in combinations of theories. Ph.D. thesis, Department of Computer Science, Saarland University (2010)","DOI":"10.1007\/978-3-642-14203-1_4"},{"key":"9567_CR72","doi-asserted-by":"crossref","unstructured":"Ihlemann, C., Sofronie-Stokkermans, V.: On hierarchical reasoning in combinations of theories. In: Automated Reasoning (IJCAR\u201910), pp. 30\u201345 (2010)","DOI":"10.1007\/978-3-642-14203-1_4"},{"key":"9567_CR73","doi-asserted-by":"crossref","unstructured":"Itzhaky, S., Banerjee, A., Immerman, N., Lahav, O., Nanevski, A., Sagiv, M.: Modular reasoning about heap paths via effectively propositional formulas. In: Principles of Programming Languages (POPL\u201914), pp. 385\u2013396 (2014)","DOI":"10.1145\/2578855.2535854"},{"key":"9567_CR74","doi-asserted-by":"crossref","unstructured":"Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: Computer Aided Verification (CAV\u201913), pp. 756\u2013772 (2013)","DOI":"10.1007\/978-3-642-39799-8_53"},{"key":"9567_CR75","doi-asserted-by":"crossref","unstructured":"Itzhaky, S., Bj\u00f8rner, N., Reps, T.W., Sagiv, M., Thakur, A.V.: Property-directed shape analysis. In: Computer Aided Verification (CAV\u201914), pp. 35\u201351 (2014)","DOI":"10.1007\/978-3-319-08867-9_3"},{"key":"9567_CR76","unstructured":"Jacobs, S.: Hierarchic decision procedures for verification. Ph.D. thesis, Department of Computer Science, Saarland University (2009)"},{"key":"9567_CR77","doi-asserted-by":"crossref","unstructured":"Karbyshev, A., Bj\u00f8rner, N., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. In: Computer Aided Verification (CAV\u201915), pp. 583\u2013602 (2015)","DOI":"10.1007\/978-3-319-21690-4_40"},{"issue":"4","key":"9567_CR78","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/BF02579150","volume":"4","author":"N Karmarkar","year":"1984","unstructured":"Karmarkar, N.: A new polynomial-time algorithm for linear programming. Combinatorica 4(4), 373\u2013395 (1984)","journal-title":"Combinatorica"},{"issue":"1","key":"9567_CR79","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1016\/0041-5553(80)90061-0","volume":"20","author":"LG Khachiyan","year":"1980","unstructured":"Khachiyan, L.G.: Polynomial algorithms in linear programming. USSR Comput. Math. Math. Phys. 20(1), 53\u201372 (1980)","journal-title":"USSR Comput. Math. Math. Phys."},{"issue":"3","key":"9567_CR80","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1145\/3242953.3242958","volume":"5","author":"E Kiero\u0144ski","year":"2018","unstructured":"Kiero\u0144ski, E., Pratt-Hartmann, I., Tendera, L.: Two-variable logics with counting and semantic constraints. SIGLOG News 5(3), 22\u201343 (2018)","journal-title":"SIGLOG News"},{"key":"9567_CR81","doi-asserted-by":"crossref","unstructured":"Korovin, K.: Non-cyclic sorts for first-order satisfiability. In: Frontiers of Combining Systems (FroCoS\u201913), LNCS 8152, pp. 214\u2013228. Springer (2013)","DOI":"10.1007\/978-3-642-40885-4_15"},{"key":"9567_CR82","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-50497-0","volume-title":"Decision Procedures","author":"D Kroening","year":"2016","unstructured":"Kroening, D., Strichman, O.: Decision Procedures. Texts in Theoretical Computer Science. An EATCS Series, 2nd edn. Springer, Berlin (2016)","edition":"2"},{"key":"9567_CR83","unstructured":"Kruglov, E.: Superposition modulo theory. Ph.D. thesis, Department of Computer Science, Saarland University (2013)"},{"issue":"4","key":"9567_CR84","doi-asserted-by":"crossref","first-page":"427","DOI":"10.1007\/s11786-012-0135-4","volume":"6","author":"E Kruglov","year":"2012","unstructured":"Kruglov, E., Weidenbach, C.: Superposition decides the first-order logic fragment over ground theories. Math. Comput. Sci. 6(4), 427\u2013456 (2012)","journal-title":"Math. Comput. Sci."},{"key":"9567_CR85","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Piskac, R., Suter, P., Wies, T.: Building a calculus of data structures. In: Verification, Model Checking, and Abstract Interpretation (VMCAI\u201910), pp. 26\u201344 (2010)","DOI":"10.1007\/978-3-642-11319-2_6"},{"key":"9567_CR86","unstructured":"Lamotte-Schubert, M.: Automatic authorization analysis. Ph.D. thesis, Department of Computer Science, Saarland University (2015)"},{"issue":"2","key":"9567_CR87","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1093\/logcom\/exu074","volume":"27","author":"M Lamotte-Schubert","year":"2017","unstructured":"Lamotte-Schubert, M., Weidenbach, C.: BDI: a new decidable clause class. J. Log. Comput. 27(2), 441\u2013468 (2017)","journal-title":"J. Log. Comput."},{"issue":"3","key":"9567_CR88","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"HR Lewis","year":"1980","unstructured":"Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci. 21(3), 317\u2013353 (1980)","journal-title":"J. Comput. Syst. Sci."},{"key":"9567_CR89","unstructured":"Lewis, H.R.: A logic of concrete time intervals (extended abstract). In: Logic in Computer Science (LICS\u201990), pp. 380\u2013389 (1990)"},{"issue":"5","key":"9567_CR90","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R Loos","year":"1993","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J. 36(5), 450\u2013462 (1993)","journal-title":"Comput. J."},{"key":"9567_CR91","unstructured":"Mahfoudh, M.: Sur la V\u00e9rification de la Satisfaction pour la Logique des Diff\u00e9rences. Ph.D. thesis, Universit\u00e9 Joseph Fourier \u2013 Grenoble 1 (2003)"},{"key":"9567_CR92","unstructured":"Mahfoudh, M., Niebert, P., Asarin, E., Maler, O.: A satisfiability checker for difference logic. In: Theory and Applications of Satisfiability Testing (SAT\u201902), pp. 222\u2013230 (2002)"},{"key":"9567_CR93","doi-asserted-by":"crossref","unstructured":"Manna, Z., Zarba, C.G.: Combining decision procedures. In: Formal Methods at the Crossroads. From Panacea to Foundational Support, 10th Anniversary Colloquium of UNU\/IIST, the International Institute for Software Technology of The United Nations University, Lisbon, Portugal, Revised Papers, pp. 381\u2013422 (2002)","DOI":"10.1007\/978-3-540-40007-3_24"},{"issue":"1","key":"9567_CR94","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1002\/malq.19750210118","volume":"21","author":"M Mortimer","year":"1975","unstructured":"Mortimer, M.: On languages with two variables. Math. Log. Q. 21(1), 135\u2013140 (1975)","journal-title":"Math. Log. Q."},{"issue":"9","key":"9567_CR95","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"LM de Moura","year":"2011","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"9567_CR96","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1090\/conm\/029\/11","volume":"29","author":"G Nelson","year":"1984","unstructured":"Nelson, G.: Combining satisfiability procedures by equality-sharing. Contemp. Math. 29, 201\u2013211 (1984)","journal-title":"Contemp. Math."},{"issue":"2","key":"9567_CR97","doi-asserted-by":"crossref","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. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9567_CR98","doi-asserted-by":"crossref","unstructured":"Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of timed automata via satisfiability checking. In: Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT\u201902), pp. 225\u2013244 (2002)","DOI":"10.1007\/3-540-45739-9_15"},{"key":"9567_CR99","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Computer Aided Verification (CAV\u201905), pp. 321\u2013334 (2005)","DOI":"10.1007\/11513988_33"},{"key":"9567_CR100","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"DC Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, convexity and combinations of theories. Theor. Comput. Sci. 12, 291\u2013302 (1980)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"9567_CR101","doi-asserted-by":"crossref","first-page":"685","DOI":"10.2307\/2695037","volume":"66","author":"M Otto","year":"2001","unstructured":"Otto, M.: Two variable first-order logic over ordered domains. J. Symb. Log. 66(2), 685\u2013702 (2001)","journal-title":"J. Symb. Log."},{"key":"9567_CR102","doi-asserted-by":"crossref","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: Programming Language Design and Implementation (PLDI\u201916), pp. 614\u2013630 (2016)","DOI":"10.1145\/2980983.2908118"},{"key":"9567_CR103","unstructured":"P\u00e9rez, J.A.N., Voronkov, A.: Encodings of bounded LTL model checking in effectively propositional logic. In: Automated Deduction (CADE-21), pp. 346\u2013361 (2007)"},{"key":"9567_CR104","unstructured":"P\u00e9rez, J.A.N., Voronkov, A.: Encodings of problems in effectively propositional logic. In: Theory and Applications of Satisfiability Testing (SAT\u201907), p.\u00a03 (2007)"},{"key":"9567_CR105","unstructured":"P\u00e9rez, J.A.N., Voronkov, A.: Proof systems for effectively propositional logic. In: Automated Reasoning (IJCAR\u201908), pp. 426\u2013440 (2008)"},{"key":"9567_CR106","doi-asserted-by":"crossref","unstructured":"P\u00e9rez, J.A.N., Voronkov, A.: Planning with effectively propositional logic. In: Programming Logics\u2014Essays in Memory of Harald Ganzinger, LNCS 7797, pp. 302\u2013316 (2013)","DOI":"10.1007\/978-3-642-37651-1_13"},{"issue":"4","key":"9567_CR107","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/s10817-009-9161-6","volume":"44","author":"R Piskac","year":"2010","unstructured":"Piskac, R., de Moura, L.M., Bj\u00f8rner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reason. 44(4), 401\u2013424 (2010)","journal-title":"J. Autom. Reason."},{"key":"9567_CR108","doi-asserted-by":"crossref","first-page":"896","DOI":"10.2178\/jsl\/1344862166","volume":"77","author":"A Policriti","year":"2012","unstructured":"Policriti, A., Omodeo, E.: The Bernays\u2013Sch\u00f6nfinkel\u2013Ramsey class for set theory: decidability. J. Symb Log. 77, 896\u2013918 (2012)","journal-title":"J. Symb Log."},{"key":"9567_CR109","unstructured":"Pratt, V.R.: Two easy theories whose combination is hard. Technical report, Massachusetts Institute of Technology (1977)"},{"issue":"1","key":"9567_CR110","doi-asserted-by":"crossref","first-page":"39","DOI":"10.2307\/2964057","volume":"22","author":"H Putnam","year":"1957","unstructured":"Putnam, H.: Decidability and essential undecidability. J. Symb. Log. 22(1), 39\u201354 (1957)","journal-title":"J. Symb. Log."},{"key":"9567_CR111","doi-asserted-by":"crossref","unstructured":"Quaas, K., Shirmohammadi, M., Worrell, J.: Revisiting reachability in timed automata. In: Logic in Computer Science (LICS\u201917), pp. 1\u201312 (2017)","DOI":"10.1109\/LICS.2017.8005098"},{"key":"9567_CR112","first-page":"1","volume":"141","author":"MO Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1\u201335 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"9567_CR113","doi-asserted-by":"crossref","unstructured":"Ranise, S., Ringeissen, C., Tran, D.: Nelson\u2013Oppen, Shostak and the extended canonizer: a family picture with a newborn. In: Theoretical Aspects of Computing (ICTAC\u201904), Revised Selected Papers, pp. 372\u2013386 (2004)","DOI":"10.1007\/978-3-540-31862-0_27"},{"key":"9567_CR114","doi-asserted-by":"crossref","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Frontiers of Combining Systems (FroCoS\u201905), pp. 48\u201364 (2005)","DOI":"10.1007\/11559306_3"},{"key":"9567_CR115","doi-asserted-by":"crossref","unstructured":"Rebele, T., Suchanek, F.M., Hoffart, J., Biega, J., Kuzey, E., Weikum, G.: YAGO: A multilingual knowledge base from Wikipedia, Wordnet, and Geonames. In: The Semantic Web (ISWC\u201916), pp. 177\u2013185 (2016)","DOI":"10.1007\/978-3-319-46547-0_19"},{"key":"9567_CR116","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting Enumerative Instantiation. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201918), pp. 112\u2013131 (2018)","DOI":"10.1007\/978-3-319-89963-3_7"},{"key":"9567_CR117","doi-asserted-by":"crossref","unstructured":"Reynolds, A., Iosif, R., Serban, C.: Reasoning in the Bernays\u2013Sch\u00f6nfinkel\u2013Ramsey fragment of separation logic. In: Verification, Model Checking, and Abstract Interpretation (VMCAI\u201917), pp. 462\u2013482 (2017)","DOI":"10.1007\/978-3-319-52234-0_25"},{"issue":"3","key":"9567_CR118","doi-asserted-by":"crossref","first-page":"500","DOI":"10.1007\/s10703-017-0290-y","volume":"51","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., King, T., Kuncak, V.: Solving quantified linear arithmetic by counterexample-guided instantiation. Form. Methods Syst. Des. 51(3), 500\u2013532 (2017)","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"9567_CR119","doi-asserted-by":"crossref","first-page":"98","DOI":"10.2307\/2266510","volume":"14","author":"J Robinson","year":"1949","unstructured":"Robinson, J.: Definability and decision problems in arithmetic. J. Symb. Log. 14(2), 98\u2013114 (1949)","journal-title":"J. Symb. Log."},{"key":"9567_CR120","unstructured":"Rue\u00df, H., Shankar, N.: Deconstructing Shostak. In: Logic in Computer Science (LICS\u201901), pp. 19\u201328 (2001)"},{"key":"9567_CR121","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1016\/j.tcs.2013.08.001","volume":"518","author":"S Ruggieri","year":"2014","unstructured":"Ruggieri, S., Eirinakis, P., Subramani, K., Wojciechowski, P.J.: On the complexity of quantified linear systems. Theor. Comput. Sci. 518, 128\u2013134 (2014)","journal-title":"Theor. Comput. Sci."},{"key":"9567_CR122","series-title":"Wiley-Interscience Series in Discrete Mathematics and Optimization","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1999","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley-Interscience Series in Discrete Mathematics and Optimization. Wiley, Hoboken (1999)"},{"key":"9567_CR123","first-page":"477","volume":"27","author":"D Scott","year":"1962","unstructured":"Scott, D.: A decision method for validity of sentences in two variables. J. Symb. Log. 27, 477 (1962)","journal-title":"J. Symb. Log."},{"key":"9567_CR124","doi-asserted-by":"crossref","unstructured":"Shankar, N., Rue\u00df, H.: Combining Shostak theories. In: Rewriting Techniques and Applications (RTA\u201902), pp. 1\u201318 (2002)","DOI":"10.1007\/3-540-45610-4_1"},{"issue":"3","key":"9567_CR125","doi-asserted-by":"crossref","first-page":"379","DOI":"10.2307\/1971037","volume":"102","author":"S Shelah","year":"1975","unstructured":"Shelah, S.: The monadic theory of order. Ann. Math. 102(3), 379\u2013419 (1975)","journal-title":"Ann. Math."},{"issue":"1","key":"9567_CR126","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"RE Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. J. ACM 31(1), 1\u201312 (1984)","journal-title":"J. ACM"},{"key":"9567_CR127","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Automated Deduction (CADE-20), pp. 219\u2013234 (2005)","DOI":"10.1007\/11532231_16"},{"key":"9567_CR128","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: On combinations of local theory extensions. In: Programming Logics\u2014Essays in Memory of Harald Ganzinger, LNCS 7797 pp. 392\u2013413 (2013)","DOI":"10.1007\/978-3-642-37651-1_16"},{"key":"9567_CR129","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: Hierarchical reasoning in local theory extensions and applications. In: Symbolic and Numeric Algorithms for Scientific Computing (SYNASC\u201914), pp. 34\u201341 (2014)","DOI":"10.1109\/SYNASC.2014.13"},{"key":"9567_CR130","doi-asserted-by":"crossref","unstructured":"Strichman, O., Seshia, S.A., Bryant, R.E.: Deciding separation formulas with SAT. In: Computer Aided Verification (CAV\u201902), pp. 209\u2013222 (2002)","DOI":"10.1007\/3-540-45657-0_16"},{"issue":"3\u20134","key":"9567_CR131","doi-asserted-by":"crossref","first-page":"483","DOI":"10.1007\/s11786-017-0319-z","volume":"11","author":"T Sturm","year":"2017","unstructured":"Sturm, T.: A survey of some methods for real quantifier elimination, decision, and satisfiability and their applications. Math. Comput. Sci. 11(3\u20134), 483\u2013502 (2017)","journal-title":"Math. Comput. Sci."},{"key":"9567_CR132","doi-asserted-by":"crossref","unstructured":"Sturm, T., Voigt, M., Weidenbach, C.: Deciding first-order satisfiability when universal and existential variables are separated. In: Logic in Computer Science (LICS\u201916), pp. 86\u201395. IEEE\/ACM (2016). An extended version is available at the arXiv\u00a0preprint server under the signature arXiv:1511.08999 [cs.LO]","DOI":"10.1145\/2933575.2934532"},{"issue":"3","key":"9567_CR133","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/j.websem.2008.06.001","volume":"6","author":"FM Suchanek","year":"2008","unstructured":"Suchanek, F.M., Kasneci, G., Weikum, G.: YAGO: a large ontology from Wikipedia and WordNet. J. Web Semant. 6(3), 203\u2013217 (2008)","journal-title":"J. Web Semant."},{"key":"9567_CR134","doi-asserted-by":"crossref","unstructured":"Suda, M., Weidenbach, C., Wischnewski, P.: On the saturation of YAGO. In: Automated Reasoning (IJCAR\u201910), pp. 441\u2013456 (2010)","DOI":"10.1007\/978-3-642-14203-1_38"},{"key":"9567_CR135","doi-asserted-by":"crossref","unstructured":"Talupur, M., Sinha, N., Strichman, O., Pnueli, A.: Range allocation for separation logic. In: Computer Aided Verification (CAV\u201904), pp. 148\u2013161 (2004)","DOI":"10.1007\/978-3-540-27813-9_12"},{"key":"9567_CR136","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson\u2013Oppen combination procedure. In: Frontiers of Combining Systems (FroCoS\u201996), pp. 103\u2013119 (1996)","DOI":"10.1007\/978-94-009-0349-4_5"},{"issue":"1","key":"9567_CR137","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 290(1), 291\u2013353 (2003)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"9567_CR138","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.G.: Combining nonstably infinite theories. J. Autom. Reason. 34(3), 209\u2013238 (2005)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9567_CR139","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1016\/j.jsc.2008.10.006","volume":"45","author":"D Tran","year":"2010","unstructured":"Tran, D., Ringeissen, C., Ranise, S., Kirchner, H.: Combination of convex theories: modularity, deduction completeness, and explanation. J. Symb. Comput. 45(2), 261\u2013286 (2010)","journal-title":"J. Symb. Comput."},{"key":"9567_CR140","doi-asserted-by":"crossref","unstructured":"Voigt, M.: The Bernays\u2013Sch\u00f6nfinkel\u2013Ramsey fragment with bounded difference constraints over the reals is decidable. In: Frontiers of Combining Systems (FroCoS\u201917), LNCS 10483, pp. 244\u2013261 (2017). An extended version is available at the arXiv\u00a0preprint server under the signature arXiv:1706.08504 [cs.LO]","DOI":"10.1007\/978-3-319-66167-4_14"},{"key":"9567_CR141","doi-asserted-by":"crossref","unstructured":"Voigt, M.: A fine-grained hierarchy of hard problems in the separated fragment. In: Logic in Computer Science (LICS\u201917), pp. 1\u201312. IEEE\/ACM (2017). An extended version is available at the arXiv\u00a0preprint server under the signature arXiv:1704.02145 [cs.LO]","DOI":"10.1109\/LICS.2017.8005094"},{"key":"9567_CR142","doi-asserted-by":"publisher","unstructured":"Voigt, M.: Decidable fragments of first-order logic and of first-order linear arithmetic with uninterpreted predicates. Ph.D. thesis, Department of Computer Science, Saarland University (2019). https:\/\/doi.org\/10.22028\/D291-28428","DOI":"10.22028\/D291-28428"},{"key":"9567_CR143","unstructured":"Voigt, M.: Separateness of variables\u2014a novel perspective on decidable first-order fragments (2019). Submitted. A preprint version is available at the arXiv\u00a0preprint server under the signature arXiv:1911.11500 [cs.LO]"},{"key":"9567_CR144","unstructured":"Voigt, M., Weidenbach, C.: Bernays\u2013Sch\u00f6nfinkel\u2013Ramsey with simple bounds is NEXPTIME-complete. ArXiv preprint arXiv:1501.07209 [cs.LO] (2015). http:\/\/arxiv.org\/abs\/1501.07209"},{"key":"9567_CR145","doi-asserted-by":"crossref","unstructured":"Wang, C., Gupta, A., Ganai, M.K.: Predicate learning and selective theory deduction for a difference logic solver. In: Design Automation Conference (DAC\u201906), pp. 235\u2013240 (2006)","DOI":"10.1145\/1146909.1146971"},{"issue":"1\/2","key":"9567_CR146","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0747-7171(88)80003-8","volume":"5","author":"V Weispfenning","year":"1988","unstructured":"Weispfenning, V.: The complexity of linear problems in fields. J. Symb. Comput. 5(1\/2), 3\u201327 (1988)","journal-title":"J. Symb. Comput."},{"key":"9567_CR147","doi-asserted-by":"crossref","unstructured":"Wies, T., Piskac, R., Kuncak, V.: Combining theories with shared set operations. In: Frontiers of Combining Systems (FroCoS\u201909), LNCS 5749, pp. 366\u2013382. Springer (2009)","DOI":"10.1007\/978-3-642-04222-5_23"},{"key":"9567_CR148","unstructured":"Wischnewski, P.: Efficient reasoning procedures for complex first-order theories. Ph.D. thesis, Department of Computer Science, Saarland University (2012)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09567-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-020-09567-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09567-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,18]],"date-time":"2021-07-18T00:04:30Z","timestamp":1626566670000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-020-09567-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,18]]},"references-count":148,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,3]]}},"alternative-id":["9567"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09567-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2020,7,18]]},"assertion":[{"value":"23 April 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 June 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 July 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}