{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T20:36:32Z","timestamp":1761510992707},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662460801"},{"type":"electronic","value":"9783662460818"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46081-8_24","type":"book-chapter","created":{"date-parts":[[2014,12,11]],"date-time":"2014-12-11T09:25:44Z","timestamp":1418289944000},"page":"431-448","source":"Crossref","is-referenced-by-count":4,"title":["A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets"],"prefix":"10.1007","author":[{"given":"Khalil","family":"Ghorbal","sequence":"first","affiliation":[]},{"given":"Andrew","family":"Sogokon","sequence":"additional","affiliation":[]},{"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"6","key":"24_CR1","doi-asserted-by":"publisher","first-page":"1002","DOI":"10.1145\/235809.235813","volume":"43","author":"S. Basu","year":"1996","unstructured":"Basu, S., Pollack, R., Roy, M.F.: On the combinatorial and algebraic complexity of quantifier elimination. J. ACM\u00a043(6), 1002\u20131045 (1996)","journal-title":"J. ACM"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"issue":"3","key":"24_CR3","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"G.E. Collins","year":"1991","unstructured":"Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput.\u00a012(3), 299\u2013328 (1991)","journal-title":"J. Symb. Comput."},{"key":"24_CR4","unstructured":"Cox, D.A., Little, J., O\u2019Shea, D.: Ideals, Varieties, and Algorithms - an introduction to computational algebraic geometry and commutative algebra, 2nd edn. Springer (1997)"},{"issue":"1","key":"24_CR5","first-page":"151","volume":"2","author":"J.G. Darboux","year":"1878","unstructured":"Darboux, J.G.: M\u00e9moire sur les \u00e9quations diff\u00e9rentielles alg\u00e9briques du premier ordre et du premier degr\u00e9. Bulletin des Sciences Math\u00e9matiques et Astronomiques\u00a02(1), 151\u2013200 (1878), http:\/\/eudml.org\/doc\/84988","journal-title":"Bulletin des Sciences Math\u00e9matiques et Astronomiques"},{"issue":"1\/2","key":"24_CR6","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"J.H. Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput.\u00a05(1\/2), 29\u201335 (1988)","journal-title":"J. Symb. Comput."},{"key":"24_CR7","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1006\/jsco.1997.0123","volume":"24","author":"A. Dolzmann","year":"1995","unstructured":"Dolzmann, A., Sturm, T.: Simplification of quantifier-free formulas over ordered fields. Journal of Symbolic Computation\u00a024, 209\u2013231 (1995)","journal-title":"Journal of Symbolic Computation"},{"key":"24_CR8","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/780506.780516","volume-title":"ISSAC","author":"J.C. Faug\u00e8re","year":"2002","unstructured":"Faug\u00e8re, J.C.: A new efficient algorithm for computing Gr\u00f6bner bases without reduction to zero (F5). In: ISSAC, pp. 75\u201383. ACM, New York (2002)"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol.\u00a08413, pp. 279\u2013294. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54862-8_19"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Ghorbal, K., Sogokon, A., Platzer, A.: A hierarchy of proof rules for checking differential invariance of algebraic sets. Tech. Rep. CMU-CS-14-140, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA (November 2014), http:\/\/reports-archive.adm.cs.cmu.edu\/anon\/2014\/abstracts\/14-140.html","DOI":"10.21236\/ADA624901"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Ghorbal, K., Sogokon, A., Platzer, A.: Invariance of conjunctions of polynomial equalities for algebraic differential equations. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol.\u00a08723, pp. 151\u2013167. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-319-10936-7_10"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Goriely, A.: Integrability and Nonintegrability of Dynamical Systems. Advanced series in nonlinear dynamics. World Scientific (2001)","DOI":"10.1142\/3846"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Lie, S.: Vorlesungen \u00fcber continuierliche Gruppen mit Geometrischen und anderen Anwendungen. Teubner, Leipzig (1893)","DOI":"10.5962\/bhl.title.18549"},{"key":"24_CR14","first-page":"454","volume":"116","author":"E. Lindel\u00f6f","year":"1894","unstructured":"Lindel\u00f6f, E.: Sur l\u2019application de la m\u00e9thode des approximations successives aux \u00e9quations diff\u00e9rentielles ordinaires du premier ordre. Comptes rendus hebdomadaires des s\u00e9ances de l\u2019Acad\u00e9mie des sciences\u00a0116, 454\u2013458 (1894)","journal-title":"Comptes rendus hebdomadaires des s\u00e9ances de l\u2019Acad\u00e9mie des sciences"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT, pp. 97\u2013106. ACM (2011)","DOI":"10.1145\/2038642.2038659"},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-642-15769-1_23","volume-title":"Static Analysis","author":"N. Matringe","year":"2010","unstructured":"Matringe, N., Moura, A.V., Rebiha, R.: Generating invariants for non-linear hybrid systems by linear algebraic methods. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 373\u2013389. Springer, Heidelberg (2010)"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"400","DOI":"10.1007\/BFb0029002","volume-title":"STACS 89","author":"E.W. Mayr","year":"1989","unstructured":"Mayr, E.W.: Membership in polynomial ideals over Q is exponential space complete. In: Cori, R., Monien, B. (eds.) STACS 1989. LNCS, vol.\u00a0349, pp. 400\u2013406. Springer, Heidelberg (1989)"},{"key":"24_CR18","unstructured":"Nagumo, M.: \u00dcber die Lage der Integralkurven gew\u00f6hnlicher Differentialgleichungen. Proceedings of the Physico-Mathematical Society of Japan\u00a024, 551\u2013559 (1942) (in German)"},{"key":"24_CR19","unstructured":"Olver, P.J.: Applications of Lie Groups to Differential Equations. Springer (2000)"},{"issue":"2","key":"24_CR20","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A. Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning\u00a041(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"24_CR21","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1093\/logcom\/exn070","volume":"20","author":"A. Platzer","year":"2010","unstructured":"Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput.\u00a020(1), 309\u2013352 (2010)","journal-title":"J. Log. Comput."},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Platzer, A.: The complete proof theory of hybrid systems. In: LICS, pp. 541\u2013550. IEEE (2012)","DOI":"10.1109\/LICS.2012.64"},{"key":"24_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-642-32347-8_3","volume-title":"Interactive Theorem Proving","author":"A. Platzer","year":"2012","unstructured":"Platzer, A.: A differential operator approach to equational differential invariants - (invited paper). In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 28\u201348. Springer, Heidelberg (2012)"},{"issue":"4","key":"24_CR24","first-page":"1","volume":"8","author":"A. Platzer","year":"2012","unstructured":"Platzer, A.: The structure of differential invariants and differential cut elimination. Logical Methods in Computer Science\u00a08(4), 1\u201338 (2012)","journal-title":"Logical Methods in Computer Science"},{"key":"24_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-540-70545-1_17","volume-title":"Computer Aided Verification","author":"A. Platzer","year":"2008","unstructured":"Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 176\u2013189. Springer, Heidelberg (2008)"},{"issue":"1","key":"24_CR26","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/s10703-007-0046-1","volume":"32","author":"S. Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Form. Methods Syst. Des.\u00a032(1), 25\u201355 (2008)","journal-title":"Form. Methods Syst. Des."},{"key":"24_CR27","unstructured":"Taly, A., Tiwari, A.: Deductive verification of continuous dynamical systems. In: FSTTCS. LIPIcs, vol.\u00a04, pp. 383\u2013394 (2009)"},{"key":"24_CR28","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A decision method for elementary algebra and geometry. Bull. Amer. Math. Soc. 59 (1951)","DOI":"10.1525\/9780520348097"},{"issue":"1","key":"24_CR29","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10703-007-0044-3","volume":"32","author":"A. Tiwari","year":"2008","unstructured":"Tiwari, A.: Abstractions for hybrid systems. Form. Methods Syst. Des.\u00a032(1), 57\u201383 (2008)","journal-title":"Form. Methods Syst. Des."},{"key":"24_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0601-9","volume-title":"Ordinary Differential Equations","author":"W. Walter","year":"1998","unstructured":"Walter, W.: Ordinary Differential Equations. Springer, New York (1998)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46081-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,30]],"date-time":"2023-07-30T15:55:35Z","timestamp":1690732535000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46081-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662460801","9783662460818"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46081-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}