使用直觉主义模态逻辑的开放互模拟刻画
计算机科学中的逻辑
2023-06-22 v7
摘要
开放互模拟是针对可能出现自由变量的开放进程项定义的。其核心思想是，为了刻画开放互模拟，我们转向直觉主义模态逻辑的设置。所引入的直觉主义模态逻辑称为 ，其模态在替换下封闭，从而诱导出称为直觉主义遗传（intuitionistic hereditary）的性质。直觉主义遗传在逻辑中反映了检查开放互模拟时所执行的自由变量的惰性实例化。关于我们的直觉主义模态逻辑，开放互模拟的可靠性证明在 Abella 中机械化。完备性证明的构造性内容给出了一个生成区分公式的算法，我们已予以实现。我们提请注意这样一个事实：存在一系列可由直觉主义模态逻辑刻画的互模拟同余。
引用
@article{arxiv.1701.05324,
title = {A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic},
author = {Ki Yung Ahn and Ross Horne and Alwen Tiu},
journal= {arXiv preprint arXiv:1701.05324},
year = {2023}
}