{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T20:36:22Z","timestamp":1761510982250,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,11,21]],"date-time":"2012-11-21T00:00:00Z","timestamp":1353456000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"name":"National Science Foundation","award":["1054246"],"award-info":[{"award-number":["1054246"]}]},{"name":"National Science Foundation","award":["0926181"],"award-info":[{"award-number":["0926181"]}]},{"name":"National Science Foundation","award":["0931985"],"award-info":[{"award-number":["0931985"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>The biggest challenge in hybrid systems verification is the handling of\ndifferential equations. Because computable closed-form solutions only exist for\nvery simple differential equations, proof certificates have been proposed for\nmore scalable verification. Search procedures for these proof certificates are\nstill rather ad-hoc, though, because the problem structure is only understood\npoorly. We investigate differential invariants, which define an induction\nprinciple for differential equations and which can be checked for invariance\nalong a differential equation just by using their differential structure,\nwithout having to solve them. We study the structural properties of\ndifferential invariants. To analyze trade-offs for proof search complexity, we\nidentify more than a dozen relations between several classes of differential\ninvariants and compare their deductive power. As our main results, we analyze\nthe deductive power of differential cuts and the deductive power of\ndifferential invariants with auxiliary differential variables. We refute the\ndifferential cut elimination hypothesis and show that, unlike standard cuts,\ndifferential cuts are fundamental proof principles that strictly increase the\ndeductive power. We also prove that the deductive power increases further when\nadding auxiliary differential variables to the dynamics.<\/jats:p>","DOI":"10.2168\/lmcs-8(4:16)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T13:21:33Z","timestamp":1385731293000},"source":"Crossref","is-referenced-by-count":17,"title":["The Structure of Differential Invariants and Differential Cut Elimination"],"prefix":"10.46298","volume":"Volume 8, Issue 4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7238-5710","authenticated-orcid":false,"given":"Andre","family":"Platzer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2012,11,21]]},"reference":[{"key":"603:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/809\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/809\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:56:36Z","timestamp":1681242996000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/809"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,11,21]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(4:16)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1104.1987","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1104.1987","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,11,21]]},"article-number":"809"}}