关于寻找 Herbrand 析取式证伪赋值的复杂性

假设 $\Phi$ 是一个一致的句子。那么不存在 $\neg \Phi$ 的 Herbrand 证明，这意味着由 $\neg \Phi$ 的前束范式构成的任何 Herbrand 析取式都是可证伪的。我们表明，寻找此类证伪赋值的问题在以下意义上是困难的：对于每一个全多项式搜索问题 $R$，都存在一个一致的 $\Phi$，使得寻找 $R$ 的解可以归约为寻找由 $\neg \Phi$ 构成的 Herbrand 析取式的证伪赋值。有人猜想不存在完全的全多项式搜索问题。如果该猜想成立，那么对于每一个一致的句子 $\Phi$，都存在一个一致的句子 $\Psi$，使得与 $\Psi$ 相关的搜索问题不能归约为与 $\Phi$ 相关的搜索问题。