pi-演算中双模拟与模态逻辑的证明搜索规范

我们在包含 nabla 量词（用于编码通用判断）和定义（用于编码不动点）的逻辑中，为有限 pi-演算规定了操作语义与双模拟关系。由于我们限定于有限情形，该逻辑展开不动点的能力使其对操作语义的归纳性质和双模拟的余归纳性质均完备。nabla 量词有助于处理 pi-演算表达式及其执行（证明）中变量作用域这一微妙问题。我们展示了该逻辑所允许的逻辑规范的若干优点：它们自然且声明式；在保持对变量完全形式化处理的同时不含关于变量名的副作用条件；早期与晚期双模拟关系之间的差异源于熟悉的逻辑区分；三个量词（全称、存在和 nabla）及其作用域之间的交互可以解释早期与晚期双模拟之间的差异以及基于受限输入和输出动作的各种模态算子之间的差异；涉及推理规则应用、统一和回溯的证明搜索可以为一阶转移、双模拟和模态逻辑满足性提供完备的证明系统。我们还展示了如何在包含归纳与余归纳的扩展逻辑中对带复制的 pi-演算进行编码。