使用直觉主义模态逻辑对开放双模似性进行表征
摘要：开放式等价性是针对可能出现自由变量的开放过程表达式进行定义的。观点是，为了描述开放式等价性，我们转向直觉主义模态逻辑的设置。所引入的直觉主义模态逻辑称为$mathcal{OM}$，其中的模态逻辑是在替换下封闭的，这引入了一种称为直觉主义继承性的属性。直觉主义继承性在逻辑上反映了在检查开放式等价性时执行的惰性实例化的自由变量。我们在Abella中对开放式等价性相对于我们的直觉主义模态逻辑的音实性证明进行了机械化。完备性证明的构造性内容提供了一种生成区分公式的算法，我们已经实现了。我们要指出的是，可以通过直觉主义模态逻辑来描述一系列等价性相容关系。
作者：Ki Yung Ahn, Ross Horne, Alwen Tiu
论文ID：1701.05324
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22