{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T19:25:32Z","timestamp":1725909932404},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661667"},{"type":"electronic","value":"9783319661674"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66167-4_14","type":"book-chapter","created":{"date-parts":[[2017,8,28]],"date-time":"2017-08-28T11:15:18Z","timestamp":1503918918000},"page":"244-261","source":"Crossref","is-referenced-by-count":5,"title":["The Bernays\u2013Sch\u00f6nfinkel\u2013Ramsey Fragment with Bounded Difference Constraints over the Reals Is Decidable"],"prefix":"10.1007","author":[{"given":"Marco","family":"Voigt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,29]]},"reference":[{"issue":"2","key":"14_CR1","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. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"14_CR2","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":"14_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-642-38574-2_3","volume-title":"Automated Deduction \u2013 CADE-24","author":"P Baumgartner","year":"2013","unstructured":"Baumgartner, P., Waldmann, U.: Hierarchic superposition with weak abstraction. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 39\u201357. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-38574-2_3"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427\u2013442. Springer, Heidelberg (2005). doi: 10.1007\/11609773_28"},{"key":"14_CR5","unstructured":"Downey, P.J.: Undecidability of Presburger arithmetic with a single monadic predicate letter. Technical report, Center for Research in Computer Technology, Harvard University (1972)"},{"issue":"4","key":"14_CR6","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":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 306\u2013320. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-02658-4_25"},{"key":"14_CR8","volume-title":"Ramsey Theory","author":"RL Graham","year":"1990","unstructured":"Graham, R.L., Rothschild, B.L., Spencer, J.H.: Ramsey Theory, 2nd edn. A Wiley-Interscience publication, New York (1990)","edition":"2"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Horbach, M., Voigt, M., Weidenbach, C.: On the combination of the Bernays-Sch\u00f6nfinkel-Ramsey fragment with simple linear integer arithmetic. In: Automated Deduction (CADE-26) (to appear)","DOI":"10.1007\/978-3-319-63046-5_6"},{"key":"14_CR10","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":"14_CR11","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","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, Heidelberg (2016). doi: 10.1007\/978-3-662-50497-0","edition":"2"},{"issue":"4","key":"14_CR12","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":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/3-540-45739-9_15","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"P Niebert","year":"2002","unstructured":"Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of timed automata via satisfiability checking. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 225\u2013243. Springer, Heidelberg (2002). doi: 10.1007\/3-540-45739-9_15"},{"key":"14_CR14","unstructured":"Pratt, V.R.: Two Easy Theories Whose Combination is Hard. Technical report, Massachusetts Institute of Technology (1977)"},{"issue":"1","key":"14_CR15","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. Symbolic Logic 22(1), 39\u201354 (1957)","journal-title":"J. Symbolic Logic"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Voigt, M.: The Bernays-Sch\u00f6nfinkel-Ramsey Fragment with Bounded Difference Constraints over the Reals is Decidable. ArXiv preprint, arXiv:1706.08504 [cs.LO] (2017)","DOI":"10.1007\/978-3-319-66167-4_14"},{"key":"14_CR17","unstructured":"Voigt, M., Weidenbach, C.: Bernays-Sch\u00f6nfinkel-Ramsey with Simple Bounds is NEXPTIME-complete. ArXiv preprint, arXiv:1501.07209 [cs.LO] (2015)"}],"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-319-66167-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T21:14:40Z","timestamp":1570050880000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66167-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661667","9783319661674"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66167-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}