{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T22:29:23Z","timestamp":1790116163173,"version":"4.0.1"},"publisher-location":"Cham","reference-count":9,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319214009","type":"print"},{"value":"9783319214016","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21401-6_32","type":"book-chapter","created":{"date-parts":[[2015,7,24]],"date-time":"2015-07-24T10:13:46Z","timestamp":1437732826000},"page":"467-481","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["A Uniform Substitution Calculus for Differential Dynamic Logic"],"prefix":"10.1007","author":[{"given":"Andr\u00e9","family":"Platzer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,7,25]]},"reference":[{"issue":"2","key":"32_CR1","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"32_CR2","volume-title":"Introduction to Mathematical Logic","author":"A Church","year":"1956","unstructured":"Church, A.: Introduction to Mathematical Logic, vol. I. Princeton University Press, Princeton (1956)"},{"issue":"3","key":"32_CR3","doi-asserted-by":"publisher","first-page":"201","DOI":"10.2307\/2267403","volume":"18","author":"L Henkin","year":"1953","unstructured":"Henkin, L.: Banishing the rule of substitution for functional variables. J. Symb. Log. 18(3), 201\u2013208 (1953)","journal-title":"J. Symb. Log."},{"issue":"2","key":"32_CR4","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. Reas. 41(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reas."},{"issue":"1","key":"32_CR5","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. 20(1), 309\u2013352 (2010)","journal-title":"J. Log. Comput."},{"key":"32_CR6","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"},{"issue":"4","key":"32_CR7","first-page":"1","volume":"8","author":"A Platzer","year":"2012","unstructured":"Platzer, A.: The structure of differential invariants and differential cut elimination. Log. Meth. Comput. Sci. 8(4), 1\u201338 (2012)","journal-title":"Log. Meth. Comput. Sci."},{"key":"32_CR8","unstructured":"Platzer, A.: Differential game logic. CoRR abs\/1408.1980 (2014)"},{"key":"32_CR9","doi-asserted-by":"crossref","unstructured":"Platzer, A.: A uniform substitution calculus for differential dynamic logic. CoRR abs\/1503.01981 (2015)","DOI":"10.1007\/978-3-319-21401-6_32"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-25"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21401-6_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T13:26:21Z","timestamp":1676467581000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-21401-6_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319214009","9783319214016"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21401-6_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"25 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}