{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:36:12Z","timestamp":1725903372787},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"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-63046-5_6","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"77-94","source":"Crossref","is-referenced-by-count":8,"title":["On the Combination of the Bernays\u2013Sch\u00f6nfinkel\u2013Ramsey Fragment with Simple Linear Integer Arithmetic"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Horbach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Voigt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"issue":"2","key":"6_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. Symbolic Comput. 45(2), 153\u2013172 (2010)","journal-title":"J. Symbolic Comput."},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-24246-0_5","volume-title":"Frontiers of Combining Systems","author":"G Alagi","year":"2015","unstructured":"Alagi, G., Weidenbach, C.: NRCL \u2013 A model building approach to\u00a0the Bernays-Sch\u00f6nfinkel fragment. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS, vol. 9322, pp. 69\u201384. Springer, Cham (2015). doi: 10.1007\/978-3-319-24246-0_5"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-04222-5_5","volume-title":"Frontiers of Combining Systems","author":"E Althaus","year":"2009","unstructured":"Althaus, E., Kruglov, E., Weidenbach, C.: Superposition modulo linear arithmetic SUP(LA). In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 84\u201399. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-04222-5_5"},{"key":"6_CR4","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":"6_CR5","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":"6_CR6","unstructured":"Bradley, A.R.: Safety Analysis of Systems. PhD thesis (2007)"},{"key":"6_CR7","unstructured":"Bradley, A.R., Manna, Z.: The Calculus of Computation \u2013 Decision Procedures with Applications to Verification. Springer, Heidelberg (2007)"},{"key":"6_CR8","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":"6_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-22438-6_17","volume-title":"Automated Deduction \u2013 CADE-23","author":"K Claessen","year":"2011","unstructured":"Claessen, K., Lilliestr\u00f6m, A., Smallbone, N.: Sort it out with monotonicity. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 207\u2013221. Springer, Heidelberg (2011). doi: 10.1007\/978-3-642-22438-6_17"},{"key":"6_CR10","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":"6_CR11","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":"6_CR12","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., 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"},{"issue":"2","key":"6_CR13","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. Symbolic Logic 56(2), 637\u2013642 (1991)","journal-title":"J. Symbolic Logic"},{"key":"6_CR14","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. ArXiv preprint, arXiv: 1705.08792 [cs.LO] (2017)","DOI":"10.1007\/978-3-319-63046-5_6"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-642-37651-1_10","volume-title":"Programming Logics","author":"K Korovin","year":"2013","unstructured":"Korovin, K.: Inst\u2013Gen \u2013 A modular approach to instantiation-based automated reasoning. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 239\u2013270. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-37651-1_10"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-40885-4_15","volume-title":"Frontiers of Combining Systems","author":"K Korovin","year":"2013","unstructured":"Korovin, K.: Non-cyclic sorts for first-order satisfiability. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 214\u2013228. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40885-4_15"},{"key":"6_CR17","doi-asserted-by":"crossref","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"},{"issue":"4","key":"6_CR18","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."},{"issue":"3","key":"6_CR19","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."},{"issue":"5","key":"6_CR20","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":"6_CR21","doi-asserted-by":"crossref","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53, 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Piskac, R., de Moura, L.M., Bj\u00f8rner, N.: Deciding effectively propositional logic using DPLL and substitution sets. J. Autom. Reasoning 44(4), 401\u2013424 (2010)","DOI":"10.1007\/s10817-009-9161-6"},{"issue":"1","key":"6_CR23","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":"6_CR24","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","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,29]],"date-time":"2019-09-29T08:26:40Z","timestamp":1569745600000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}