{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T00:35:42Z","timestamp":1767141342239,"version":"build-2238731810"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2016,9,23]],"date-time":"2016-09-23T00:00:00Z","timestamp":1474588800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,9,23]],"date-time":"2016-09-23T00:00:00Z","timestamp":1474588800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1305054"],"award-info":[{"award-number":["CCF-1305054"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006831","name":"U.S. Air Force","doi-asserted-by":"publisher","award":["FA9550-12-1-0199"],"award-info":[{"award-number":["FA9550-12-1-0199"]}],"id":[{"id":"10.13039\/100006831","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004895","name":"European Social Fund","doi-asserted-by":"publisher","award":["and Greek national funds through the Operational Program Education and Lifelong Learning of the National Strategic Reference Framework (NSRF) - Research Funding Program: Thales - MIS: 380232"],"award-info":[{"award-number":["and Greek national funds through the Operational Program Education and Lifelong Learning of the National Strategic Reference Framework (NSRF) - Research Funding Program: Thales - MIS: 380232"]}],"id":[{"id":"10.13039\/501100004895","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2017,3]]},"DOI":"10.1007\/s10472-016-9525-7","type":"journal-article","created":{"date-parts":[[2016,9,23]],"date-time":"2016-09-23T11:36:53Z","timestamp":1474630613000},"page":"245-266","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Analyzing restricted fragments of the theory of linear arithmetic"],"prefix":"10.1007","volume":"79","author":[{"given":"Piotr","family":"Wojciechowski","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5262-7265","authenticated-orcid":false,"given":"Pavlos","family":"Eirinakis","sequence":"additional","affiliation":[]},{"given":"K.","family":"Subramani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,23]]},"reference":[{"key":"9525_CR1","volume-title":"Existential theory of the reals, volume 10 of algorithms and computation in mathematics","author":"S Basu","year":"2006","unstructured":"Basu, S., Pollack, R., Roy, M.-F.: Existential theory of the reals, volume 10 of algorithms and computation in mathematics. Springer, Berlin (2006)"},{"key":"9525_CR2","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. Theor. Comput. Sci. 11, 71\u201377 (1980)","journal-title":"Theor. Comput. Sci."},{"issue":"8","key":"9525_CR3","doi-asserted-by":"publisher","first-page":"1004","DOI":"10.1287\/mnsc.30.8.1004","volume":"30","author":"WF Bialas","year":"1984","unstructured":"Bialas, W.F., Karwan, M.H.: Two-level linear programming. Manag. Sci. 30(8), 1004\u20131020 (1984)","journal-title":"Manag. Sci."},{"key":"9525_CR4","volume-title":"The calculus of computation - decision procedures with applications to verification","author":"AR Bradley","year":"2007","unstructured":"Bradley, A.R., Manna, Z.: The calculus of computation - decision procedures with applications to verification, first edition. Springer, Berlin (2007)","edition":"first edition"},{"issue":"4","key":"9525_CR5","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/968708.968710","volume":"37","author":"CW Brown","year":"2003","unstructured":"Brown, C.W.: QEPCAD B: A Program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bull. 37(4), 97\u2013108 (2003)","journal-title":"ACM SIGSAM Bull."},{"issue":"1","key":"9525_CR6","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"HK B\u00fcning","year":"1995","unstructured":"B\u00fcning, H.K., Karpinski, M., Fl\u00f6gel, A.: Resolution for quantified boolean formulas. Inf. Comput. 117(1), 12\u201318 (1995)","journal-title":"Inf. Comput."},{"key":"9525_CR7","doi-asserted-by":"crossref","unstructured":"Canny, J.: Some algebraic and geometric computations in PSPACE. Proceedings of the Twentieth Annual ACM Symposium on Theory of Computing, 460\u2013467 (1988)","DOI":"10.1145\/62212.62257"},{"issue":"1","key":"9525_CR8","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/A:1008133505376","volume":"19","author":"S Choi","year":"2000","unstructured":"Choi, S., Agrawala, A.: Dynamic dispatching of cyclic real-time tasks with relative timing constraints. Real-Time Syst. 19(1), 5\u201340 (2000)","journal-title":"Real-Time Syst."},{"issue":"3","key":"9525_CR9","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"GE Collins","year":"1991","unstructured":"Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299\u2013328 (1991)","journal-title":"J. Symb. Comput."},{"issue":"1-2","key":"9525_CR10","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"JH Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1-2), 29\u201335 (1988)","journal-title":"J. Symb. Comput."},{"issue":"2","key":"9525_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 Bull. 31(2), 2\u20139 (1997)","journal-title":"ACM SIGSAM Bull."},{"issue":"3","key":"9525_CR12","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1023\/A:1006031329384","volume":"21","author":"A Dolzmann","year":"1998","unstructured":"Dolzmann, A., Sturm, T., Weispfenning, V.: A new approach for automatic theorem proving in real geometry. J. Autom. Reason. 21(3), 357\u2013380 (1998)","journal-title":"J. Autom. Reason."},{"key":"9525_CR13","doi-asserted-by":"crossref","unstructured":"Dolzmann, A., Sturm, T., Weispfenning, V.: Real quantifier elimination in practice. In: Matzat, B.H., et al. (eds.) Algorithmic Algebra and Number Theory, pages 221\u2013248. Springer (1998)","DOI":"10.1007\/978-3-642-59932-3_11"},{"issue":"4","key":"9525_CR14","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/s10472-013-9332-3","volume":"71","author":"P Eirinakis","year":"2014","unstructured":"Eirinakis, P., Ruggieri, S., Subramani, K., Wojciechowski, P.: On quantified linear implications. Ann. Math. Artif. Intell. 71(4), 301\u2013325 (2014)","journal-title":"Ann. Math. Artif. Intell."},{"issue":"1","key":"9525_CR15","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1137\/0204006","volume":"4","author":"J Ferrante","year":"1975","unstructured":"Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM J. Comput. 4(1), 69\u201376 (1975)","journal-title":"SIAM J. Comput."},{"issue":"3","key":"9525_CR16","doi-asserted-by":"publisher","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."},{"issue":"3","key":"9525_CR17","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1023\/A:1016372507161","volume":"9","author":"RJ Hall","year":"2002","unstructured":"Hall, R.J.: Specification, validation, and synthesis of email agent controllers: A case study in function rich reactive system design. Autom. Softw. Eng. 9(3), 233\u2013261 (2002)","journal-title":"Autom. Softw. Eng."},{"key":"9525_CR18","first-page":"39","volume":"2937","author":"D Harel","year":"2004","unstructured":"Harel, D.: A grand challenge for computing: Towards full reactive modeling of a multi-cellular animal. Verification, Model Checking, Abstr. Interpretation 2937, 39\u201360 (2004)","journal-title":"Verification, Model Checking, Abstr. Interpretation"},{"key":"9525_CR19","doi-asserted-by":"crossref","unstructured":"Kam, N., Cohen, I.R., Harel, D.: The immune system as a reactive system: modeling t cell activation with statecharts. In: Proceedings of the 2001 IEEE Symposia on Human-Centric Computing Languages and Environments, pp. 15\u201322 (2001)","DOI":"10.1109\/HCC.2001.995228"},{"key":"9525_CR20","first-page":"1093","volume":"224","author":"LG Khachiyan","year":"1979","unstructured":"Khachiyan, L.G.: A polynomial algorithm in linear programming. Doklady Akademiia Nauk SSSR 224, 1093\u20131096 (1979). English Translation: Soviet Mathematics Doklady, Volume 20, pp. 1093\u20131096","journal-title":"Doklady Akademiia Nauk SSSR"},{"key":"9525_CR21","doi-asserted-by":"crossref","unstructured":"Koo, T.J., Sinopoli, B., Sangiovanni-Vincentelli, A., Sastry, S.: A formal approach to reactive system design: unmanned aerial vehicle flight management system design example. In: Proceedings of the 1999 IEEE International Symposium on Computer Aided Control System Design, pp. 522\u2013527 (1999)","DOI":"10.1109\/CACSD.1999.808702"},{"key":"9525_CR22","unstructured":"Christos, H.: Papadimitriou computational complexity Addison-Wesley (1994)"},{"key":"9525_CR23","doi-asserted-by":"crossref","unstructured":"Pfitzmann, B., Waidner, M.: Composition and integrity preservation of secure reactive systems. In: Proceedings of the 2000 ACM Conference on Computer Communications Security, pp. 245\u2013254 (2000)","DOI":"10.1145\/352600.352639"},{"key":"9525_CR24","doi-asserted-by":"crossref","unstructured":"Pfitzmann, B., Waidner, M.: A model for asynchronous reactive systems and its application to secure message transmission. In: Proceedings of the 2001 IEEE Symposium on Security and Privacy, pp. 184\u2013200 (2001)","DOI":"10.1109\/SECPRI.2001.924298"},{"issue":"4","key":"9525_CR25","doi-asserted-by":"publisher","first-page":"723","DOI":"10.1145\/1183278.1183282","volume":"7","author":"S Ratschan","year":"2006","unstructured":"Ratschan, S.: Efficient solving of quantified inequality constraints over the real numbers. ACM Trans. Comput. Log. 7(4), 723\u2013748 (2006)","journal-title":"ACM Trans. Comput. Log."},{"key":"9525_CR26","unstructured":"Ratschan, S.: RSOLVER. http:\/\/rsolver.sourceforge.net (2013)"},{"issue":"3","key":"9525_CR27","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/582475.582484","volume":"33","author":"M Schaefer","year":"2002","unstructured":"Schaefer, M., Umans, C.: Completeness in the polynomial-time hierarchy A compendium. SIGACT News 33(3), 32\u201349 (2002)","journal-title":"SIGACT News"},{"issue":"4","key":"9525_CR28","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/601819.601829","volume":"33","author":"M Schaefer","year":"2002","unstructured":"Schaefer, M., Umans, C.: Completeness in the polynomial-time hierarchy Part II. SIGACT News 33(4), 22\u201336 (2002)","journal-title":"SIGACT News"},{"key":"9525_CR29","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":"9525_CR30","first-page":"531","volume":"4","author":"PW Shor","year":"1991","unstructured":"Shor, P.W.: Stretchability of pseudolines is NP-hard. DIMACS 4, 531\u2013534 (1991)","journal-title":"DIMACS"},{"issue":"3","key":"9525_CR31","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(85)90076-6","volume":"20","author":"ED Sontag","year":"1985","unstructured":"Sontag, E.D.: Real addition and the polynomial hierarchy. Inf. Process. Lett. 20 (3), 115\u2013120 (1985)","journal-title":"Inf. Process. Lett."},{"key":"9525_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"LJ Stockmeyer","year":"1977","unstructured":"Stockmeyer, L.J.: The polynomial-time hierarchy. Theor. Comput. Sci. 3, 1\u201322 (1977)","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"9525_CR33","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/s10472-007-9085-y","volume":"51","author":"K Subramani","year":"2007","unstructured":"Subramani, K.: On a decision procedure for quantified linear programs. Ann. Math. Artif. Intell. 51(1), 55\u201377 (2007)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9525_CR34","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Technical report r-109 rand corporation (1948)"},{"issue":"1-2","key":"9525_CR35","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0747-7171(88)80003-8","volume":"4","author":"V Weispfenning","year":"1988","unstructured":"Weispfenning, V.: The complexity of linear problems in fields. J. Symb. Comput. 4(1-2), 3\u201327 (1988)","journal-title":"J. Symb. Comput."}],"updated-by":[{"DOI":"10.1007\/s10472-017-9537-y","type":"erratum","label":"Erratum","source":"publisher","updated":{"date-parts":[[2017,3,3]],"date-time":"2017-03-03T00:00:00Z","timestamp":1488499200000}}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-016-9525-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-016-9525-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-016-9525-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,10]],"date-time":"2025-06-10T17:02:24Z","timestamp":1749574944000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-016-9525-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,23]]},"references-count":35,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2017,3]]}},"alternative-id":["9525"],"URL":"https:\/\/doi.org\/10.1007\/s10472-016-9525-7","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9,23]]},"assertion":[{"value":"23 September 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}