类型导向的否定消除

在模态μ演算中，若每个递归变量出现在偶数个否定之下，则公式是良构的。借助德摩根律，可轻易将任意良构公式转换为等价的无否定公式——其否定范式。此外，若公式大小为 n，其否定范式大小同为 O(n)。因此，完整模态μ演算与否定范式片段具有同等的表达力与简洁性。本文将该结果扩展至高阶模态不动点逻辑(HFL)——一种带有高阶递归谓词变换器的模态μ演算扩展。我们提出一种过程，将公式转换为无否定的等价公式，最坏情况下为二次大小，而当公式变量数固定时为线性大小。