{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:52:29Z","timestamp":1762458749568},"publisher-location":"Berlin, Heidelberg","reference-count":12,"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_5","type":"book-chapter","created":{"date-parts":[[2009,9,16]],"date-time":"2009-09-16T16:42:11Z","timestamp":1253119331000},"page":"84-99","source":"Crossref","is-referenced-by-count":34,"title":["Superposition Modulo Linear Arithmetic SUP(LA)"],"prefix":"10.1007","author":[{"given":"Ernst","family":"Althaus","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Evgeny","family":"Kruglov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Weidenbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"5_CR1","doi-asserted-by":"publisher","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.\u00a010(1), 129\u2013179 (2009)","journal-title":"ACM Trans. Comput. Log."},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1007\/978-3-642-02011-7_6","volume-title":"SEA 2009","author":"E. Althaus","year":"2009","unstructured":"Althaus, E., Dumitriu, D.: Fast and accurate bounds on linear programs. In: Vahrenhold, J. (ed.) SEA 2009. LNCS, vol.\u00a05526, pp. 40\u201350. Springer, Heidelberg (2009)"},{"issue":"3\/4","key":"5_CR3","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. Applicable Algebra in Engineering, Communication and Computing, AAECC\u00a05(3\/4), 193\u2013212 (1994)","journal-title":"Applicable Algebra in Engineering, Communication and Computing, AAECC"},{"key":"5_CR4","unstructured":"Dimova, D.: On the translation of timed automata into first-order logic. In: Fietzke, A., Weidenbach, C. (supervisors) (2009)"},{"key":"5_CR5","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":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-540-79719-7_8","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2008","author":"G. Faure","year":"2008","unstructured":"Faure, G., Nieuwenhuis, R., Oliveras, A., Rodr\u00edguez-Carbonell, E.: Sat modulo the theory of linear arithmetic: Exact, inexact and commercial solvers. In: Kleine B\u00fcning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol.\u00a04996, pp. 77\u201390. Springer, Heidelberg (2008)"},{"key":"5_CR7","first-page":"251","volume":"1","author":"U. Hustadt","year":"2004","unstructured":"Hustadt, U., Schmidt, R.A., Georgieva, L.: A survey of decidable first-order fragments and description logics. Journal of Relational Methods in Computer Science\u00a01, 251\u2013276 (2004)","journal-title":"Journal of Relational Methods in Computer Science"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K. Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 223\u2013237. Springer, Heidelberg (2007)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/3-540-46430-1_30","volume-title":"Hybrid Systems: Computation and Control","author":"A. Nonnengart","year":"2000","unstructured":"Nonnengart, A.: Hybrid systems verification by location elimination. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol.\u00a01790, pp. 352\u2013365. Springer, Heidelberg (2000)"},{"key":"5_CR10","volume-title":"Theory of linear and integer programming","author":"A. Schrijver","year":"1989","unstructured":"Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons, Inc., Chichester (1989)"},{"key":"5_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/3-540-45744-5_17","volume-title":"Automated Reasoning","author":"U. Waldmann","year":"2001","unstructured":"Waldmann, U.: Superposition and chaining for totally ordered divisible abelian groups. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 226\u2013241. Springer, Heidelberg (2001)"},{"key":"5_CR12","doi-asserted-by":"publisher","first-page":"1965","DOI":"10.1016\/B978-044450813-3\/50029-1","volume-title":"Handbook of Automated Reasoning, ch.\u00a027","author":"C. Weidenbach","year":"2001","unstructured":"Weidenbach, C.: Combining superposition, sorts and splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch.\u00a027, vol.\u00a02, pp. 1965\u20132012. Elsevier, Amsterdam (2001)"}],"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_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T22:46:22Z","timestamp":1552171582000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04222-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642042218","9783642042225"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04222-5_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}