This paper introduces a uniform substitution calculus for differential refinement logic dRL. The logic dRL extends the differential dynamic logic dL such that one can simultaneously reason about properties of and relations between hybrid systems. Refinements are useful e.g. for simplifying proofs by relating a concrete hybrid system to an abstract one from which the property can be proved more easily. Uniform substitution is the key to parsimonious prover microkernels. It enables the verbatim use of single axiom formulas instead of axiom schemata with soundness-critical side conditions scattered across the proof calculus. The uniform substitution rule can then be used to instantiate all axioms soundly. Access to differential variables in dRL enables more control over the notion of refinement, which is shown to be decidable on a fragment of hybrid programs.

翻译：本文介绍了微分精化逻辑dRL的统一替换演算。该逻辑dRL扩展了微分动态逻辑dL，使得人们能够同时推理混合系统的性质及其之间的关系。精化在证明中非常有用，例如通过将具体混合系统与抽象混合系统相关联来简化证明，因为从抽象系统可以更容易地证明性质。统一替换是构建简洁证明器微内核的关键。它允许逐字使用单个公理公式，而不是使用在证明演算中散布着对可靠性至关重要的边条件的公理模式。然后，统一替换规则可用于可靠地实例化所有公理。在dRL中访问微分变量使得对精化概念有更多的控制，这被证明在混合程序的一个片段上是可判定的。