一次性均匀替换
计算机科学中的逻辑
2019-08-06 v3 编程语言
逻辑
摘要
函数、谓词、程序或博弈符号的均匀替换是混合系统与混合博弈的极简证明器的核心操作。通过推迟对可靠性至关重要的可接纳性检查，本文引入了一种沿公式同态地以线性遍次进行的均匀替换机制。可靠性通过对替换所执行替换处的一个简单变量条件得以恢复。本文的设定是微分混合博弈，其中离散、连续与对抗动力学在微分博弈逻辑 dGL 中相互作用。本文证明了 dGL 的一次性均匀替换的可靠性与完备性。
引用
@article{arxiv.1902.07230,
title = {Uniform Substitution At One Fell Swoop},
author = {André Platzer},
journal= {arXiv preprint arXiv:1902.07230},
year = {2019}
}
备注
CADE 2019 Extending arXiv:1804.05880 with differential games arXiv:1507.04943