{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:54:39Z","timestamp":1725490479741},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540751861"},{"type":"electronic","value":"9783540751878"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75187-8_22","type":"book-chapter","created":{"date-parts":[[2007,9,1]],"date-time":"2007-09-01T15:13:38Z","timestamp":1188659618000},"page":"275-294","source":"Crossref","is-referenced-by-count":3,"title":["Weak Integer Quantifier Elimination Beyond the Linear Case"],"prefix":"10.1007","author":[{"given":"Aless","family":"Lasaruk","sequence":"first","affiliation":[]},{"given":"Thomas","family":"Sturm","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du premier congres de Mathematiciens des Pays Slaves, Warsaw, Poland, pp. 92\u2013101 (1929)"},{"key":"22_CR2","first-page":"91","volume":"7","author":"D.C. Cooper","year":"1972","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. Machine Intelligence\u00a07, 91\u201399 (1972)","journal-title":"Machine Intelligence"},{"key":"22_CR3","first-page":"27","volume":"7","author":"M. Fischer","year":"1974","unstructured":"Fischer, M., Rabin, M.: Super-exponential complexity of Presburger arithmetic. SIAM-AMS Proceedings\u00a07, 27\u201341 (1974)","journal-title":"SIAM-AMS Proceedings"},{"key":"22_CR4","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1137\/0204006","volume":"4","author":"J. Ferrante","year":"1975","unstructured":"Ferrante, J., Rackoff, C.W.: A decision procedure for the first-order theory of real addition with order. SIAM Journal on Computing\u00a04, 69\u201377 (1975)","journal-title":"SIAM Journal on Computing"},{"key":"22_CR5","series-title":"Lecture Notes in Mathematics","volume-title":"The Computational Complexity of Logical Theories","year":"1979","unstructured":"Ferrante, J., Rackoff, C.W. (eds.): The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol.\u00a0718. Springer, Berlin (1979)"},{"key":"22_CR6","doi-asserted-by":"publisher","first-page":"155","DOI":"10.2307\/2042554","volume":"72","author":"J. zur Gathen von","year":"1978","unstructured":"von zur Gathen, J., Sieveking, M.: A bound on solutions of linear integer equalities and inequalities. Proceedings of the AMS\u00a072, 155\u2013158 (1978)","journal-title":"Proceedings of the AMS"},{"key":"22_CR7","first-page":"95","volume-title":"FOCS 1977","author":"L. Berman","year":"1977","unstructured":"Berman, L.: Precise bounds for Presburger arithmetic and the reals with addition. In: FOCS 1977. 18th Annual Symposium on Foundations of Computer Science, Providence, RI, USA, October 3\u2013November 2, pp. 95\u201399. IEEE Press, Los Alamitos (1977)"},{"key":"22_CR8","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0304-3975(80)90037-7","volume":"11","author":"L. Berman","year":"1980","unstructured":"Berman, L.: The complexity of logical theories. Theoretical Computer Science\u00a011, 71\u201377 (1980)","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"22_CR9","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1016\/S0747-7171(08)80051-X","volume":"10","author":"V. Weispfenning","year":"1990","unstructured":"Weispfenning, V.: The complexity of almost linear diophantine problems. Journal of Symbolic Computation\u00a010(5), 395\u2013403 (1990)","journal-title":"Journal of Symbolic Computation"},{"key":"22_CR10","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1145\/258726.258746","volume-title":"ISSAC 1997","author":"V. Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Complexity and uniformity of elimination in Presburger Arithmetic. In: K\u00fcchlin, W.W. (ed.) ISSAC 1997. Proceedings of the 1997 International Symposium on Symbolic and Algebraic Computation, Maui, HI, pp. 48\u201353. ACM Press, New York, NY (1997)"},{"issue":"1&2","key":"22_CR11","doi-asserted-by":"publisher","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. Journal of Symbolic Computation\u00a05(1&2), 3\u201327 (1988)","journal-title":"Journal of Symbolic Computation"},{"issue":"5","key":"22_CR12","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 (special issue on computational quantifier elimination). The Computer Journal\u00a036(5), 450\u2013462 (1993)","journal-title":"The Computer Journal"},{"issue":"2","key":"22_CR13","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002000050055","volume":"8","author":"V. Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra\u2014the quadratic case and beyond. Applicable Algebra in Engineering Communication and Computing\u00a08(2), 85\u2013101 (1997)","journal-title":"Applicable Algebra in Engineering Communication and Computing"},{"issue":"2","key":"22_CR14","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1006\/jsco.1999.0303","volume":"30","author":"T. Sturm","year":"2000","unstructured":"Sturm, T.: Linear problems in valued fields. Journal of Symbolic Computation\u00a030(2), 207\u2013219 (2000)","journal-title":"Journal of Symbolic Computation"},{"key":"22_CR15","unstructured":"Seidl, A.M., Sturm, T.: Boolean quantification in a first-order context. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing. Proceedings of the CASC 2003, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany, pp. 329\u2013345 (2003)"},{"key":"22_CR16","unstructured":"Lasaruk, A., Sturm, T.: Weak quantifier elimination for the full linear theory of the integers. a uniform generalization of presburger arithmetic. Technical Report MIP-0604, FMI, Universit\u00e4t Passau, D-94030 Passau, Germany (2006) (to appear in the journal AAECC)"},{"issue":"2","key":"22_CR17","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":"22_CR18","unstructured":"Dolzmann, A., Sturm, T.: Redlog user manual. Technical Report MIP-9905, FMI, Universit\u00e4t Passau, D-94030 Passau, Germany, Edition 2.0 for Version 2.0 (1999)"},{"key":"22_CR19","unstructured":"Dolzmann, A., Sturm, T.: Generalized constraint solving over differential algebras. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing. Proceedings of the CASC 2004, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany, pp. 111\u2013125 (2004)"},{"key":"22_CR20","first-page":"239","volume-title":"Rhine Workshop on Computer Algebra. Proceedings of the RWCA 2006","author":"C. Stra\u00dfer","year":"2006","unstructured":"Stra\u00dfer, C.: Quantifier elimination for queues. In: Draisma, J., Kraft, H. (eds.) Rhine Workshop on Computer Algebra. Proceedings of the RWCA 2006, pp. 239\u2013248. Universit\u00e4t Basel, Basel (2006)"},{"key":"22_CR21","first-page":"221","volume-title":"Algorithmic Algebra and Number Theory","author":"A. Dolzmann","year":"1998","unstructured":"Dolzmann, A., Sturm, T., Weispfenning, V.: Real quantifier elimination in practice. In: Matzat, B.H., Greuel, G.M., Hiss, G. (eds.) Algorithmic Algebra and Number Theory, pp. 221\u2013247. Springer, Berlin (1998)"},{"key":"22_CR22","unstructured":"Sturm, T., Weispfenning, V.: Quantifier elimination in term algebras. The case of finite languages. In: Ganzha, V.G., Mayr, E.W., Vorozhtsov, E.V. (eds.) Computer Algebra in Scientific Computing. Proceedings of the CASC 2002, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen, Germany, pp. 285\u2013300 (2002)"},{"issue":"2","key":"22_CR23","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1006\/jsco.1997.0122","volume":"24","author":"V. Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Simulation and optimization by quantifier elimination (special issue on applications of quantifier elimination). Journal of Symbolic Computation\u00a024(2), 189\u2013208 (1997)","journal-title":"Journal of Symbolic Computation"},{"key":"22_CR24","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/309831.309894","volume-title":"ISSAC 1999","author":"A. Dolzmann","year":"1999","unstructured":"Dolzmann, A., Sturm, T.: P-adic constraint solving. In: Dooley, S. (ed.) ISSAC 1999. Proceedings of the 1999 International Symposium on Symbolic and Algebraic Computation, Vancouver, BC, pp. 151\u2013158. ACM Press, New York, NY (1999)"},{"key":"22_CR25","unstructured":"Snelting, G.: Quantifier elimination and information flow control for software security. In: Dolzmann, A., Seidl, A., Sturm, T. (eds.) Algorithmic Algebra and Logic. Proceedings of the A3L 2005, BoD, Germany, Norderstedt, pp. 237\u2013242 (2005)"},{"issue":"4","key":"22_CR26","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1145\/1178625.1178628","volume":"15","author":"G. Snelting","year":"2006","unstructured":"Snelting, G., Robschink, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. ACM Transactions on Software Engineering and Methodology\u00a015(4), 410\u2013457 (2006)","journal-title":"ACM Transactions on Software Engineering and Methodology"}],"container-title":["Lecture Notes in Computer Science","Computer Algebra in Scientific Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75187-8_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:54:45Z","timestamp":1619520885000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75187-8_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540751861","9783540751878"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75187-8_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}