{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:40:13Z","timestamp":1750308013418,"version":"3.41.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2006,10,1]],"date-time":"2006-10-01T00:00:00Z","timestamp":1159660800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2006,10]]},"abstract":"<jats:p>Let a quantified inequality constraint over the reals be a formula in the first-order predicate language over the structure of the real numbers, where the allowed predicate symbols are \u2264 and &lt;. Solving such constraints is an undecidable problem when allowing function symbols such sin or cos. In this article, we give an algorithm that terminates with a solution for all, except for very special, pathological inputs. We ensure the practical efficiency of this algorithm by employing constraint programming techniques.<\/jats:p>","DOI":"10.1145\/1183278.1183282","type":"journal-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T19:38:29Z","timestamp":1168976309000},"page":"723-748","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":63,"title":["Efficient solving of quantified inequality constraints over the real numbers"],"prefix":"10.1145","volume":"7","author":[{"given":"Stefan","family":"Ratschan","sequence":"first","affiliation":[{"name":"Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany"}]}],"member":"320","published-online":{"date-parts":[[2006,10]]},"reference":[{"volume-title":"Proceedings of the 4th IEEE Mediterranean Symposium on Control and Automation","author":"Abdallah C.","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","DOI":"10.1109\/TAC.1975.1100846","article-title":"Output feedback stabilization and related problems---solution via decision methods","author":"Anderson B. D. O.","year":"1975","journal-title":"IEEE Trans. Automatic Control AC-20, 53--66.]]"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00032-8"},{"volume-title":"Proceedings of the 35th Annual Symposium on Foundations of Computer Science, S. Goldwasser, Ed. IEEE Computer Society Press","author":"Basu S.","key":"e_1_2_1_4_1"},{"volume-title":"Constant Programming: Basic and Trends","series-title":"Lecture Notes in Computer Science","author":"Benhamou F.","key":"e_1_2_1_5_1"},{"volume":"1894","volume-title":"Proceedings of the 6th International Conference on Principles and Practice of Constraint Programming (CP'2000)","author":"Benhamou F.","key":"e_1_2_1_6_1"},{"volume-title":"Proceedings of the International Conference on Logic Programming. MIT Press","author":"Benhamou F.","key":"e_1_2_1_7_1"},{"volume-title":"International Symposium on Logic Programming.","year":"1994","author":"Benhamou F.","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0743-1066(96)00142-2","article-title":"Applying interval arithmetic to real, integer and Boolean constraints","volume":"32","author":"Benhamou F.","year":"1997","journal-title":"J. Logic Prog."},{"volume-title":"Beyond NP: Arc-consistency for quantified constraints. In Proceedings of the Principles and Practice of Constraint Programming (CP","year":"2002","author":"Bordeaux L.","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"crossref","unstructured":"Caviness B. F. and Johnson J. R. Eds. 1998. Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Wien Austria.]]  Caviness B. F. and Johnson J. R. Eds. 1998. Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer Wien Austria.]]","DOI":"10.1007\/978-3-7091-9459-1"},{"key":"e_1_2_1_12_1","first-page":"125","article-title":"Logical arithmetic","volume":"2","author":"Cleary J. G.","year":"1987","journal-title":"Future Comput. Syst."},{"key":"e_1_2_1_13_1","unstructured":"Collavizza H. Delobel F. and Rueher M. 1999. Extending consistent domains of numeric CSP. In IJCAI-99. (Stockholm Sweden).]]   Collavizza H. Delobel F. and Rueher M. 1999. Extending consistent domains of numeric CSP. In IJCAI-99. (Stockholm Sweden).]]"},{"key":"e_1_2_1_14_1","series-title":"Lecture Notes in Computer Science","volume-title":"2nd GI Conference on Automata Theory and Formal Languages","author":"Collins G. E.","year":"1998"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(08)80152-6"},{"volume-title":"Proceedings of the 1977 Symposium on Artificial Intelligence and Programming Languages. 1--12","author":"Cousot P.","key":"e_1_2_1_16_1"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0036142995281528"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80004-X"},{"key":"e_1_2_1_19_1","first-page":"5","article-title":"Quantified multivariate polynomial inequalities","volume":"20","author":"Dorato P.","year":"2000","journal-title":"IEEE Cont. Syst. Mag."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1997.0120"},{"volume-title":"Proceedings of AAAI'96","author":"Fargier H.","key":"e_1_2_1_21_1"},{"volume-title":"Proceedings of the 32nd IEEE Conference Decision and Control. IEEE Computer Society Press","author":"Fiorio G.","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Garloff J. and Graf B. 1999. Solving strict polynomial inequalities by Bernstein expansion. In The Use of Symbolic Methods in Control System Analysis and Design N. Munro Ed. The Institution of Electrical Engineering (IEE) 339--352.]]  Garloff J. and Graf B. 1999. Solving strict polynomial inequalities by Bernstein expansion. In The Use of Symbolic Methods in Control System Analysis and Design N. Munro Ed. The Institution of Electrical Engineering (IEE) 339--352.]]","DOI":"10.1049\/PBCE056E_ch14"},{"key":"e_1_2_1_24_1","first-page":"125","article-title":"A symbolic-numerical branch and prune algorithm for solving non-linear polynomial systems","volume":"4","author":"Granvilliers L.","year":"1998","journal-title":"J. Univ. Comput. Sci."},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/BF02307383","article-title":"Safe starting regions by fixed points and tightening","volume":"53","author":"Hong H.","year":"1994","journal-title":"Computing"},{"volume-title":"Proceedings of the 41st IEEE Conference on Decision and Control. IEEE Computer Society Press","year":"2002","author":"Jaulin L.","key":"e_1_2_1_26_1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Jaulin L. Kieffer M. Didrit O. and Walter \u00c9. 2001. Applied Interval Analysis with Examples in Parameter and State Estimation Robust Control and Robotics. Springer Berlin Germany.]]  Jaulin L. Kieffer M. Didrit O. and Walter \u00c9. 2001. Applied Interval Analysis with Examples in Parameter and State Estimation Robust Control and Robotics. Springer Berlin Germany.]]","DOI":"10.1007\/978-1-4471-0249-6"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","first-page":"1217","DOI":"10.1016\/0005-1098(96)00050-7","article-title":"Guaranteed tuning, with application to robust control and motion planning","volume":"32","author":"Jaulin L.","year":"1996","journal-title":"Automatica"},{"volume":"714","volume-title":"Proceedings of the 5th International Symposium on Programming Language Implementation and Logic Programming, PLILP'93","author":"Jourdan J.","key":"e_1_2_1_29_1"},{"key":"e_1_2_1_30_1","first-page":"255","article-title":"Theoretical justification of a heuristic subbox selection criterion for interval global optimization","volume":"9","author":"Kreinovich V.","year":"2001","journal-title":"Central European J. Oper. Res."},{"key":"e_1_2_1_31_1","doi-asserted-by":"crossref","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","article-title":"Applying linear quantifier elimination","volume":"36","author":"Loos R.","year":"1993","journal-title":"Comput. J."},{"key":"e_1_2_1_32_1","unstructured":"Macintyre A. and Wilkie A. 1996. On the decidability of the real exponential field. In Kreiseliana---About and Around Georg Kreisel P. Odifreddi Ed. A. K. Peters 441--467.]]  Macintyre A. and Wilkie A. 1996. On the decidability of the real exponential field. In Kreiseliana---About and Around Georg Kreisel P. Odifreddi Ed. A. K. Peters 441--467.]]"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0005-1098(97)00028-9"},{"volume":"2239","volume-title":"Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming (CP2001)","author":"Marriott K.","key":"e_1_2_1_34_1"},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","first-page":"432","DOI":"10.1093\/comjnl\/36.5.432","article-title":"Solving polynomial strict inequalities using cylindrical algebraic decomposition","volume":"36","author":"McCallum S.","year":"1993","journal-title":"Comput. J."},{"key":"e_1_2_1_36_1","unstructured":"Moore R. E. 1966. Interval Analysis. Prentice Hall Englewood Cliffs NJ.]]  Moore R. E. 1966. Interval Analysis. Prentice Hall Englewood Cliffs NJ.]]"},{"key":"e_1_2_1_37_1","doi-asserted-by":"crossref","unstructured":"Neumaier A. 1990. Interval Methods for Systems of Equations. Cambridge University Press Cambridge UK.]]  Neumaier A. 1990. Interval Methods for Systems of Equations. Cambridge University Press Cambridge UK.]]","DOI":"10.1017\/CBO9780511526473"},{"key":"e_1_2_1_38_1","volume-title":"Lecture Notes in Computer Science","volume":"910","author":"Podelski A., Ed.","year":"1995"},{"key":"e_1_2_1_39_1","unstructured":"Ratschan S. 2001a. Applications of quantified constraint solving over the reals---bibliography. http:\/\/www.mpi-sb.mpg.de\/~ratschan\/appqcs.html.]]  Ratschan S. 2001a. Applications of quantified constraint solving over the reals---bibliography. http:\/\/www.mpi-sb.mpg.de\/~ratschan\/appqcs.html.]]"},{"key":"e_1_2_1_40_1","unstructured":"Ratschan S. 2001b. Real first-order constraints are stable with probability one. http:\/\/www.mpi-sb.mpg.de\/~ratschan\/preprints.html.Draft.]]  Ratschan S. 2001b. Real first-order constraints are stable with probability one. http:\/\/www.mpi-sb.mpg.de\/~ratschan\/preprints.html.Draft.]]"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1023\/A:1014785518570","article-title":"Approximate quantified constraint solving by cylindrical box decomposition","volume":"8","author":"Ratschan S.","year":"2002","journal-title":"Rel. Comput."},{"key":"e_1_2_1_42_1","volume-title":"Eds. Lecture Notes in Computer Science","volume":"2385","author":"Ratschan S.","year":"2002"},{"key":"e_1_2_1_43_1","volume-title":"Proceedings of the 8th International Conference on Principles and Practice of Constraint Programming, P. van Hentenryck, Ed. Lecture Notes in Computer Science","volume":"2470","author":"Ratschan S.","year":"2002"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2001.0519"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1016246616462"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(10)80003-3"},{"key":"e_1_2_1_47_1","first-page":"275","article-title":"Motivations for an arbitrary precision interval arithmetic and the MPFI library. Reli","volume":"11","author":"Revol N.","year":"2005","journal-title":"Comput."},{"key":"e_1_2_1_48_1","doi-asserted-by":"crossref","first-page":"514","DOI":"10.2307\/2271358","article-title":"Some undecidable problems involving elementary functions of a real variable","volume":"33","author":"Richardson D.","year":"1968","journal-title":"J. Symb. Logic"},{"key":"e_1_2_1_49_1","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/BF00143879","article-title":"Consistency techniques for continuous constraints","volume":"1","author":"Sam-Haroud D.","year":"1996","journal-title":"Constraints"},{"key":"e_1_2_1_50_1","first-page":"323","article-title":"Outer estimation of generalized solution sets to interval linear systems. Reli","volume":"5","author":"Shary S. P.","year":"1999","journal-title":"Comput."},{"key":"e_1_2_1_51_1","first-page":"321","article-title":"A new technique in systems analysis under interval uncertainty and ambiguity. Reli","volume":"8","author":"Shary S. P.","year":"2002","journal-title":"Comput."},{"volume-title":"Proceedings of the 14th Canadian Conference on AI.]]","author":"Silaghi M.-C.","key":"e_1_2_1_52_1"},{"key":"e_1_2_1_53_1","doi-asserted-by":"crossref","unstructured":"Tarski A. 1951. A Decision Method for Elementary Algebra and Geometry. University of California Press Berkeley CA. (Also in Caviness and Johnson {1998}).]]  Tarski A. 1951. A Decision Method for Elementary Algebra and Geometry. University of California Press Berkeley CA. (Also in Caviness and Johnson {1998}).]]","DOI":"10.1525\/9780520348097"},{"key":"e_1_2_1_54_1","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1017\/S0022481200028899","article-title":"Alfred Tarski's elimination theory for real closed fields","volume":"53","author":"van den Dries L.","year":"1988","journal-title":"J. Symb. Logic"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0036142995281504"},{"key":"e_1_2_1_56_1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5073.001.0001","volume-title":"Numerica: A Modeling Language for Global Optimization","author":"Van Hentenryck P.","year":"1997"},{"volume":"910","volume-title":"Ed. Lecture Notes in Computer Science","author":"Van Hentenryck P.","key":"e_1_2_1_57_1"},{"volume-title":"Proceedings of ECAI.]]","year":"2002","author":"Walsh T.","key":"e_1_2_1_58_1"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(88)80003-8"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183278.1183282","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1183278.1183282","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:06:37Z","timestamp":1750259197000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183278.1183282"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10]]},"references-count":59,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,10]]}},"alternative-id":["10.1145\/1183278.1183282"],"URL":"https:\/\/doi.org\/10.1145\/1183278.1183282","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2006,10]]},"assertion":[{"value":"2006-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}