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 is 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中微分变量的引入增强了对精化概念的控制能力，且已证明该逻辑在混合程序的某个片段上具有可判定性。