This paper introduces a uniform substitution calculus for $d\mathcal{L}_\text{CHP}$, the dynamic logic of communicating hybrid programs. Uniform substitution enables parsimonious prover kernels by using axioms instead of axiom schemata. Instantiations can be recovered from a single proof rule responsible for soundness-critical instantiation checks rather than being spread across axiom schemata in side conditions. Even though communication and parallelism reasoning are notorious for necessitating subtle soundness-critical side conditions, uniform substitution when generalized to $d\mathcal{L}_\text{CHP}$ manages to limit and isolate their conceptual overhead. Since uniform substitution has proven to simplify the implementation of hybrid systems provers substantially, uniform substitution for $d\mathcal{L}_\text{CHP}$ paves the way for a parsimonious implementation of theorem provers for hybrid systems with communication and parallelism.

翻译：本文引入了$d\mathcal{L}_\text{CHP}$（通信混合程序的动态逻辑）的统一替换演算。统一替换通过使用公理而非公理模式，实现了简约的证明器内核。实例化可由单一的证明规则恢复，该规则负责对可靠性至关重要的实例化检查，而非散布在带有侧条件的公理模式中。尽管通信与并行推理因需要微妙的可靠性关键侧条件而著称，但当统一替换推广到$d\mathcal{L}_\text{CHP}$时，它能有效地限制并隔离这些概念上的开销。由于统一替换已被证明能大幅简化混合系统证明器的实现，$d\mathcal{L}_\text{CHP》的统一替换为构建支持通信与并行性的混合系统定理证明器的简约实现铺平了道路。