无需斯科莱姆化的Herbrand公式判定过程

本文描述了一种判定过程，用于不包含量词作用域内∨的纯一阶逻辑反前束范式合取的析取（FOLDNFs）。这些FOLDNFs的析取项等价于前束范式，其无量词部分是原子公式及其否定的合取（= Herbrand公式）。与Herbrand公式的常用算法不同，既不使用斯科莱姆化，也不使用带函数符号的合一算法。取而代之，描述了一个仅建立在纯一阶逻辑（FOL）等价变换基础上的过程。该过程涉及负范式演算（NNF演算）的应用，其中A ⊣⊢ A ∧ A（= ∧I）是唯一增加给定FOLDNFs复杂性的规则。所描述的算法展示了如何在Herbrand公式情况下，通过系统地寻找将NNF演算中∧I规则应用次数减至最小的证明来解决判定问题。在Herbrand公式情况下，甚至可以完全避免应用∧I。最后，展示了如何将所描述的过程用于优化的一般矛盾证明搜索中，以及在一般矛盾证明搜索中∧I-最小证明策略引发何种问题。