Uniform Substitution in One Fell Swoop
share
Uniform substitution of function, predicate, program or game symbols is the core operation in parsimonious provers for hybrid systems and hybrid games. By postponing soundness-critical admissibility checks does this paper introduce a uniform substitution mechanism that proceeds in a linear pass homomorphically along the formula. Soundness is recovered using a simple variable condition at the replacements performed by the substitution. The setting in this paper is that of hybrid games, in which discrete, continuous, and adversarial dynamics interact in differential game logic dGL. This paper proves soundness and completeness of one-pass uniform substitutions for dGL.
READ FULL TEXT