具有通信混合程序的动态逻辑的统一替代
摘要：一个用于动态逻辑的统一替换演算被引入。统一替换能够通过使用公理而不是公理原理来实现简化证明核心。实例化可以从负责声音关键实例化检查的单个证明规则中恢复，而不是分散在侧条件的公理原理中。尽管通信和并行推理通常需要复杂的声音关键侧条件，但是将统一替换推广到$dL\_CHP$可以限制并隔离其概念耗费。由于统一替换已经被证明可以极大地简化混合系统证明器的实现，因此对于$dL\_CHP$的统一替换为具有通信和并行功能的混合系统的定理证明器的简化实现铺平了道路。
作者：Marvin Brieger, Stefan Mitsch, Andr''e Platzer
论文ID：2303.17333
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-19