微分博弈逻辑的均匀替换
计算机科学中的逻辑
2018-07-20 v1 计算机科学与博弈论
编程语言
逻辑
摘要
本文提出微分博弈逻辑(dGL)的均匀替换演算。丘奇的均匀替换将项或公式处处替换函数或谓词符号。在将其推广到微分博弈逻辑并允许用混合博弈替换博弈符号后,均匀替换使得仅使用公理而非公理模式成为可能,从而大幅简化实现。所得公理化不采用微妙的 schema 变量以及对逻辑变量出现模式的可靠性关键旁条件来将无穷多公理模式实例限制为可靠者,而是仅采用有限个普通 dGL 公式作为公理,由均匀替换可靠地实例化。本文证明了单调模态逻辑 dGL 的均匀替换的可靠性与完备性。所得公理化允许在定理证明器中直接模块化实现 dGL。
引用
@article{arxiv.1804.05880,
title = {Uniform Substitution for Differential Game Logic},
author = {André Platzer},
journal= {arXiv preprint arXiv:1804.05880},
year = {2018}
}