{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T16:52:10Z","timestamp":1791219130475,"version":"4.1.0"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,10,11]],"date-time":"2007-10-11T00:00:00Z","timestamp":1192060800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2007,10,22]]},"DOI":"10.1007\/s10472-007-9085-y","type":"journal-article","created":{"date-parts":[[2007,10,10]],"date-time":"2007-10-10T14:13:09Z","timestamp":1192025589000},"page":"55-77","source":"Crossref","is-referenced-by-count":15,"title":["On a decision procedure for quantified linear programs"],"prefix":"10.1007","volume":"51","author":[{"given":"K.","family":"Subramani","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2007,10,11]]},"reference":[{"issue":"2","key":"9085_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994). Fundamental Study. 25\u00a0April","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"9085_CR2","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B. Aspvall","year":"1979","unstructured":"Aspvall, B., Plass, M.F., Tarjan, R.: A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inf. Process. Lett. 8(3), 121\u2013123 (1979)","journal-title":"Inf. Process. Lett."},{"key":"9085_CR3","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1016\/0305-0548(93)90013-9","volume":"20","author":"O. Ben-Ayed","year":"1993","unstructured":"Ben-Ayed, O.: Bilevel linear programming. Comput. Oper. Res. 20, 485\u2013501 (1993)","journal-title":"Comput. Oper. Res."},{"key":"9085_CR4","doi-asserted-by":"crossref","unstructured":"Benhamou, F., Goualard, F.: Universally quantified interval constraints. In: CP, pp. 67\u201382 (2000)","DOI":"10.1007\/3-540-45349-0_7"},{"key":"9085_CR5","doi-asserted-by":"crossref","unstructured":"Benhamou, F., Goulard, F.: Universally quantified interval constraints. In: Proceedings of Constraint Programming (2000) September","DOI":"10.1007\/3-540-45349-0_7"},{"issue":"1","key":"9085_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0743-1066(96)00142-2","volume":"32","author":"F. Benhamou","year":"1997","unstructured":"Benhamou, F., Older, W.J.: Applying interval arithmetic to real, integer, and boolean constraints. J. Log. Program. 32(1), 1\u201324 (1997)","journal-title":"J. Log. Program."},{"key":"9085_CR7","doi-asserted-by":"crossref","unstructured":"Cadoli, M., Giovanardi, M., Giovanardi, A., Schaerf, M.: Experimental analysis of the computational cost of evaluating quantified boolean formulae. In: Lecture Notes in Artificial Intelligence (1997)","DOI":"10.1007\/3-540-63576-9_109"},{"key":"9085_CR8","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified boolean formulae. In: AAAI-98 (1998) July"},{"key":"9085_CR9","doi-asserted-by":"crossref","DOI":"10.1002\/9781118033166","volume-title":"Optimization Methods for Logical Inference. Series in Discrete Mathematics and Optimization","author":"V. Chandru","year":"1999","unstructured":"Chandru, V., Hooker, J.N.: Optimization Methods for Logical Inference. Series in Discrete Mathematics and Optimization. John Wiley & Sons Inc., New York (1999)"},{"key":"9085_CR10","volume-title":"Algorithms and Theory of Computation Handbook","author":"V. Chandru","year":"1999","unstructured":"Chandru, V., Rao, M.R.: Linear programming. In: Algorithms and Theory of Computation Handbook. CRC Press, Boca Raton, FL (1999)"},{"key":"9085_CR11","unstructured":"Choi, S.: Dynamic time-based scheduling for hard real-time systems. Ph.D. thesis, University of Maryland, College Park (1997) June"},{"issue":"1","key":"9085_CR12","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1008133505376","volume":"19","author":"S. Choi","year":"2000","unstructured":"Choi, S., Agrawala, A.K.: Dynamic dispatching of cyclic real-time tasks with relative timing constraints. Real-Time Syst. 19(1), 5\u201340 (2000)","journal-title":"Real-Time Syst."},{"key":"9085_CR13","unstructured":"Colmerauer, A.: Logic programming and its applications, Chapter theoretical model of prologII. Ablex Series in Artificial Intelligence, pp. 181\u2013200. Ablex Publishing Corporation (1986)"},{"key":"9085_CR14","doi-asserted-by":"crossref","unstructured":"Colmerauer, A., Dao, T.: Expressiveness of full first order constraints in the algebra of finite or infinite trees. In: Proceedings of Constraint Programming (2000) September","DOI":"10.1007\/3-540-45349-0_14"},{"issue":"1","key":"9085_CR15","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/BF01384316","volume":"6","author":"J.C. Corbett","year":"1995","unstructured":"Corbett, J.C., Avrunin, G.S.: Using integer programming to verify safety and liveness properties. Form. Methods Syst. Des. 6(1), 97\u2013123 (1995)","journal-title":"Form. Methods Syst. Des."},{"key":"9085_CR16","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1016\/0097-3165(73)90004-6","volume":"14","author":"G.B. Dantzig","year":"1973","unstructured":"Dantzig, G.B., Eaves, B.C.: Fourier\u2013Motzkin elimination and its dual. J. Comb. Theory (A) 14, 288\u2013297 (1973)","journal-title":"J. Comb. Theory (A)"},{"key":"9085_CR17","unstructured":"Donald, B., Kapur, D., Mundy, J.L.: Symbolic and numerical computation for artificial intelligence. Academic Press (1992)"},{"key":"9085_CR18","unstructured":"Fourier, J.B.J.: Reported in: Analyse de Travaux de l\u2019Academie Royale des Sciences, Pendant l\u2019annee 1824, Partie Mathematique, Histoire de \u2019Academie Royale de Sciences de l\u2019Institue de France 7 (1827) xlvii-lv. (Partial English translation in: Kohler, D.A.: Translation of a report by Fourier on his work on linear inequalities. Opsearch 10, 38\u201342 (1973).). Academic Press (1824)"},{"issue":"3","key":"9085_CR19","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1109\/12.372041","volume":"44","author":"R. Gerber","year":"1995","unstructured":"Gerber, R., Pugh, W., Saksena, M.: Parametric dispatching of hard real-time tasks. IEEE Trans. Comput. 44(3), 471\u2013479 (1995)","journal-title":"IEEE Trans. Comput."},{"key":"9085_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04880-1","volume-title":"The complexity theory companion","author":"L.A. Hemaspaandra","year":"2002","unstructured":"Hemaspaandra, L.A., Ogihara, M.: The complexity theory companion. Springer-Verlag, New York (2002)"},{"issue":"6","key":"9085_CR21","doi-asserted-by":"crossref","first-page":"1179","DOI":"10.1137\/S0097539793251876","volume":"23","author":"D.S. Hochbaum","year":"1994","unstructured":"Hochbaum, D.S., (Seffi) Naor, J.: Simple and fast algorithms for linear and integer programs with two variables per inequality. SIAM J. Comput. 23(6), 1179\u20131192 (1994) December","journal-title":"SIAM J. Comput."},{"key":"9085_CR22","doi-asserted-by":"crossref","unstructured":"Hooker, J.N.: Logic-Based Methods for Optimization. Series in Discrete Mathematics and Optimization. John Wiley & Sons Inc. (2000)","DOI":"10.1002\/9781118033036"},{"key":"9085_CR23","doi-asserted-by":"crossref","unstructured":"Huynh, T., Lassez, C., Lassez, J.-L.: Fourier algorithm revisited. In: Kirchner, H., Wechler, W. (eds.) Proceedings Second International Conference on Algebraic and Logic Programming. Lecture Notes in Computer Science, vol. 463, pp. 117\u2013131. Nancy, France, Springer-Verlag (1990) October","DOI":"10.1007\/3-540-53162-9_34"},{"key":"9085_CR24","unstructured":"Lassez, C., Lassez, J.L.: Quantifier elimination for conjunctions of linear constraints via a convex hull algorithm. Academic Press (1993)"},{"key":"9085_CR25","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/BF00245296","volume":"9","author":"J.-L. Lassez","year":"1992","unstructured":"Lassez, J.-L., Maher, M.: On Fourier\u2019s algorithm for linear constraints. J. Autom. Reason. 9, 373\u2013379 (1992)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9085_CR26","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/71021.71026","volume":"23","author":"S.T. Levi","year":"1989","unstructured":"Levi, S.T., Tripathi, S.K., Carson, S.D., Agrawala, A.K.: The Maruti hard real-time operating system. ACM Spec. Interest Group on Oper. Syst. 23(3), 90\u2013106 (1989) July","journal-title":"ACM Spec. Interest Group on Oper. Syst."},{"issue":"5","key":"9085_CR27","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":"9085_CR28","unstructured":"Mosse, D., Ko, K.-T., Agrawala, A.K., Tripathi, S.K.: Maruti: an environment for hard real-time applications. In: Agrawala, A.K., Gordon, K.D., Hwang, P. (eds.) Maruti OS, pp. 75\u201385. IOS Press (1992)"},{"key":"9085_CR29","volume-title":"Integer and Combinatorial Optimization","author":"G.L. Nemhauser","year":"1999","unstructured":"Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. John Wiley & Sons, New York (1999)"},{"key":"9085_CR30","unstructured":"Papadimitriou, C.H., Steiglitz, K.: Combinatorial Optimization. Prentice Hall (1982)"},{"key":"9085_CR31","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, New York (1994)"},{"key":"9085_CR32","unstructured":"Ratschan, S.: Applications of quantified constraint solving over the reals. http:\/\/www.cs.cas.cz\/~ratschan\/preprints.html"},{"key":"9085_CR33","doi-asserted-by":"crossref","unstructured":"Ratschan, S.: Continuous first-order constraint satisfaction. In: AISC, pp. 181\u2013195 (2002)","DOI":"10.1007\/3-540-45470-5_18"},{"key":"9085_CR34","doi-asserted-by":"crossref","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. In: HSCC, pp. 573\u2013589 (2005)","DOI":"10.1007\/978-3-540-31954-2_37"},{"key":"9085_CR35","unstructured":"Saksena, M.: Parametric scheduling in hard real-time systems. Ph.D. thesis, University of Maryland, College Park (1994) June"},{"key":"9085_CR36","volume-title":"Theory of linear and Integer Programming","author":"A. Schrijver","year":"1987","unstructured":"Schrijver, A.: Theory of linear and Integer Programming. John Wiley and Sons, New York (1987)"},{"key":"9085_CR37","unstructured":"Subramani, K.: Duality in the parametric polytope and its applications to a scheduling problem. Ph.D. thesis, University of Maryland, College Park (2000) August"},{"key":"9085_CR38","doi-asserted-by":"crossref","unstructured":"Subramani, K.: Parametric scheduling \u2013 algorithms & complexity. In: Monien, B. et.\u00a0al. (eds.) Proceedings of the 8th International Conference on High-Performance Computing (Hi-PC), vol. 2228 of Lecture Notes in Computer Science, pp. 36\u201346. Springer-Verlag (2001) December","DOI":"10.1007\/3-540-45307-5_4"},{"key":"9085_CR39","doi-asserted-by":"crossref","unstructured":"Subramani, K.: A specification framework for real-time scheduling. In: Grosky, W.I., Plasil, F. (eds.) Proceedings of the 29th Annual Conference on Current Trends in Theory and Practice of Informatics (SOFSEM). Lecture Notes in Computer Science, vol. 2540, pp. 195\u2013207. Springer-Verlag (2002) November","DOI":"10.1007\/3-540-36137-5_14"},{"key":"9085_CR40","doi-asserted-by":"crossref","DOI":"10.1525\/9780520348097","volume-title":"A Decision Method for Elementary Algebra and Geometry","author":"A. Tarski","year":"1951","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry. Univ. of California Press, Berkeley (1951)"},{"key":"9085_CR41","first-page":"29","volume-title":"Proceedings of the 19th Annual ACM Symposium on Theory of Computing","author":"P.M. Vaidya","year":"1987","unstructured":"Vaidya, P.M.: An algorithm for linear programming which requires O(((m+n)n 2+(m+n)1.5 n)L) arithmetic operations. In: Aho, A. (ed.) Proceedings of the 19th Annual ACM Symposium on Theory of Computing, pp. 29\u201338. ACM Press, New York City, NY (1987) May"},{"key":"9085_CR42","volume-title":"Nonlinear Optimization: Complexity Issues","author":"S.A. Vavasis","year":"1991","unstructured":"Vavasis, S.A.: Nonlinear Optimization: Complexity Issues. Oxford University Press, New York (1991)"},{"key":"9085_CR43","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/BF01096458","volume":"5","author":"L. Vicente","year":"1994","unstructured":"Vicente, L., Calamai, P.: Bilevel and multilevel programming: a bibliography review. J. Global Optim. 5, 291\u2013306 (1994)","journal-title":"J. Global Optim."},{"issue":"2","key":"9085_CR44","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/s002000050055","volume":"8","author":"V. Weispfenning","year":"1997","unstructured":"Weispfenning, V.: Quantifier elimination for real algebra \u2013 the quadratic case and beyond. Appl. Algebra Eng. Commun. Comput. 8(2), 85\u2013101 (1997)","journal-title":"Appl. Algebra Eng. Commun. Comput."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-007-9085-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-007-9085-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-007-9085-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,25]],"date-time":"2021-08-25T15:39:06Z","timestamp":1629905946000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-007-9085-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10,11]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,10,22]]}},"alternative-id":["9085"],"URL":"https:\/\/doi.org\/10.1007\/s10472-007-9085-y","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,10,11]]}}}