{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:14:51Z","timestamp":1743138891418,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642243639"},{"type":"electronic","value":"9783642243646"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24364-6_9","type":"book-chapter","created":{"date-parts":[[2011,9,29]],"date-time":"2011-09-29T01:22:21Z","timestamp":1317259341000},"page":"119-134","source":"Crossref","is-referenced-by-count":8,"title":["Superposition Modulo Non-linear Arithmetic"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Eggers","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Evgeny","family":"Kruglov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Kupferschmid","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karsten","family":"Scheibler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tino","family":"Teige","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","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, vol.\u00a05749, pp. 84\u201399. Springer, Heidelberg (2009)"},{"issue":"3\/4","key":"9_CR2","doi-asserted-by":"publisher","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. AAECC\u00a05(3\/4), 193\u2013212 (1994)","journal-title":"AAECC"},{"key":"9_CR3","series-title":"Frontiers in Artificial Intelligence and Applications","first-page":"825","volume-title":"Handbook of Satisfiability","author":"C. Barrett","year":"2009","unstructured":"Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol.\u00a0185, ch. 26, pp. 825\u2013885. IOS Press, Amsterdam (2009)"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Bauer, A., Pister, M., Tautschnig, M.: Tool-support for the analysis of hybrid systems and models. In: DATE 2007, Nice, France, pp. 924\u2013929 (2007)","DOI":"10.1109\/DATE.2007.364411"},{"key":"9_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-89439-1_19","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. Baumgartner","year":"2008","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: ME(LIA) - model evolution with linear integer arithmetic constraints. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 258\u2013273. Springer, Heidelberg (2008)"},{"key":"9_CR6","series-title":"Foundations of Artificial Intelligence","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1016\/S1574-6526(06)80020-9","volume-title":"Handbook of Constraint Programming","author":"F. Benhamou","year":"2006","unstructured":"Benhamou, F., Granvilliers, L.: Continuous and interval constraints. In: Rossi, F., van Beek, P., Walsh, T. (eds.) Handbook of Constraint Programming. Foundations of Artificial Intelligence, ch. 16, pp. 571\u2013603. Elsevier, Amsterdam (2006)"},{"key":"9_CR7","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. CACM\u00a05, 394\u2013397 (1962)","journal-title":"CACM"},{"issue":"3","key":"9_CR8","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory. Journal of the ACM\u00a07(3), 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"key":"9_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-540-71070-7_40","volume-title":"Automated Reasoning","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Engineering DPLL(T) + saturation. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 475\u2013490. Springer, Heidelberg (2008)"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"2","key":"9_CR11","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A. Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: Redlog: Computer algebra meets computer logic. ACM SIGSAM Bulletin\u00a031(2), 2\u20139 (1997)","journal-title":"ACM SIGSAM Bulletin"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Eggers, A., Kruglov, E., Kupferschmid, S., Scheibler, K., Teige, T., Weidenbach, C.: Superposition modulo non-linear arithmetic. Report of SFB\/TR 14 AVACS\u00a080 (August 2011), http:\/\/www.avacs.org","DOI":"10.1007\/978-3-642-24364-6_9"},{"issue":"3-4","key":"9_CR13","first-page":"209","volume":"1","author":"M. Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex Boolean structure. JSAT\u00a01(3-4), 209\u2013236 (2007)","journal-title":"JSAT"},{"key":"9_CR14","unstructured":"Gao, S., Ganai, M.K., Ivancic, F., Gupta, A., Sankaranarayanan, S., Clarke, E.M.: Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems. In: FMCAD 2010 (2010)"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/3-540-46430-1_14","volume-title":"Hybrid Systems: Computation and Control","author":"T. Henzinger","year":"2000","unstructured":"Henzinger, T., Horowitz, B., Majumdar, R., Wong-Toi, H.: Beyond hytech: Hybrid systems analysis using interval numerical methods. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol.\u00a01790, pp. 130\u2013144. Springer, Heidelberg (2000)"},{"key":"9_CR16","unstructured":"Herde, C.: Efficient Solving of Large Arithmetic Constraint Systems with Complex Boolean Structure: Proof Engines for the Analysis of Hybrid Discrete\u2013Continuous Systems. Doctoral dissertation, Carlvon Ossietzky Universit\u00e4t Oldenburg (2010)"},{"issue":"4","key":"9_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1805950.1805957","volume":"11","author":"M. Horbach","year":"2010","unstructured":"Horbach, M., Weidenbach, C.: Superposition for fixed domains. ACM Transactions on Computational Logic\u00a011(4), 1\u201335 (2010)","journal-title":"ACM Transactions on Computational Logic"},{"key":"9_CR18","unstructured":"Keddis, N.: Strong satisfaction. Bachelorthesis, Albert-Ludwigs-Universit\u00e4t Freiburg (September 2008)"},{"key":"9_CR19","volume-title":"IEEE Design and Diagnostics of Electronic Circuits and Systems","author":"S. Kupferschmid","year":"2011","unstructured":"Kupferschmid, S., Becker, B., Teige, T., Fr\u00e4nzle, M.: Proof certificates and non-linear arithmetic constraints. In: IEEE Design and Diagnostics of Electronic Circuits and Systems. IEEE, Los Alamitos (2011)"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/978-3-540-71493-4_37","volume-title":"Hybrid Systems: Computation and Control","author":"A. Platzer","year":"2007","unstructured":"Platzer, A., Clarke, E.: The image computation problem in hybrid systems model checking. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 473\u2013486. Springer, Heidelberg (2007)"},{"key":"9_CR21","unstructured":"Revol, N., Rouillier, F., Chevillard, S., Lauter, C., Nguyen, H.D., Theveny, P.: Mpfi: Multiple precision floating-point interval arithmeticm, https:\/\/gforge.inria.fr\/projects\/mpfi\/"},{"issue":"4","key":"9_CR22","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/9.664154","volume":"43","author":"C.J. Tomlin","year":"1998","unstructured":"Tomlin, C.J., Pappas, G.J., Sastry, S.: Conflict resolution for air traffic management: A study in multi-agent hybrid systems. IEEE Transactions on Automatic Control\u00a043(4), 509\u2013521 (1998)","journal-title":"IEEE Transactions on Automatic Control"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02959-2_10","volume-title":"Automated Deduction \u2013 CADE-22","author":"C. Weidenbach","year":"2009","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol.\u00a05663, pp. 140\u2013145. 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-24364-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,16]],"date-time":"2019-06-16T14:00:10Z","timestamp":1560693610000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24364-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642243639","9783642243646"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24364-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}