Abstract
This paper introduces a new proof calculus for differential dynamic logic (\(\mathsf {d}\mathcal {L}\)) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to rely on axioms rather than axiom schemata, substantially simplifying implementations. Instead of subtle schema variables and soundness-critical side conditions on the occurrence patterns of variables, the resulting calculus adopts only a finite number of ordinary \(\mathsf {d}\mathcal {L}\) formulas as axioms. The static semantics of differential dynamic logic is captured exclusively in uniform substitutions and bound variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this paper introduces differential forms for differential dynamic logic that make it possible to internalize differential invariants, differential substitutions, and derivations as first-class axioms in \(\mathsf {d}\mathcal {L}\).
All proofs are in a companion report [9]. This material is based upon work supported by the National Science Foundation by NSF CAREER Award CNS-1054246.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
A slight abuse of notation rewrites the differential as \([\![{(\theta )'}]\!]^{I} = d[\![{\theta }]\!]^{I} = \sum _{i=1}^n \frac{\partial [\![\theta ]\!]^I}{\partial x^i} dx^i\) when \(x^1,\dots ,x^n\) are the variables in \(\theta \) and their differentials \(dx^i\) form the basis of the cotangent space, which, when evaluated at a point \({\nu }\) whose values \({\nu }({x}^{\prime })\) determine the tangent vector alias vector field, coincides with Definition 4.
- 3.
\( [{{{x}^{\prime }=f(x)\,} \& {\,q(x)}}]{(q(x)\rightarrow p(x))} \rightarrow [{{{x}^{\prime }=f(x)\,} \& {\,q(x)}}]{p(x)}\) derives by K from DW. The converse \( [{{{x}^{\prime }=f(x)\,} \& {\,q(x)}}]{p(x)} \rightarrow [{{{x}^{\prime }=f(x)\,} \& {\,q(x)}}]{(q(x)\rightarrow p(x))}\) derives by K since G derives \( [{{{x}^{\prime }=f(x)\,} \& {\,q(x)}}]{\big (p(x)\rightarrow (q(x)\rightarrow p(x))\big )}\).
References
Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56–68 (1940)
Church, A.: Introduction to Mathematical Logic, vol. I. Princeton University Press, Princeton (1956)
Henkin, L.: Banishing the rule of substitution for functional variables. J. Symb. Log. 18(3), 201–208 (1953)
Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reas. 41(2), 143–189 (2008)
Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309–352 (2010)
Platzer, A.: The complete proof theory of hybrid systems. In: LICS, pp. 541–550. IEEE (2012)
Platzer, A.: The structure of differential invariants and differential cut elimination. Log. Meth. Comput. Sci. 8(4), 1–38 (2012)
Platzer, A.: Differential game logic. CoRR abs/1408.1980 (2014)
Platzer, A.: A uniform substitution calculus for differential dynamic logic. CoRR abs/1503.01981 (2015)
Acknowledgment
I thank the anonymous reviewers for their helpful feedback.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Platzer, A. (2015). A Uniform Substitution Calculus for Differential Dynamic Logic. In: Felty, A., Middeldorp, A. (eds) Automated Deduction - CADE-25. CADE 2015. Lecture Notes in Computer Science(), vol 9195. Springer, Cham. https://doi.org/10.1007/978-3-319-21401-6_32
Download citation
DOI: https://doi.org/10.1007/978-3-319-21401-6_32
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-21400-9
Online ISBN: 978-3-319-21401-6
eBook Packages: Computer ScienceComputer Science (R0)