prolog - 如何写成 skolem 形式？(Prolog)

Question

将下面的公式翻译成斯科伦形式的喇叭公式:

∀w¬∀x∃z(H(w)∧(¬G(x,x)∨¬H(z)))

它是从德文翻译成英文的，如何将它写成喇叭形式然后再写成 skolem 形式，我在互联网上没有找到任何东西......请帮助我

Answer 1

我将始终使用 skolemization 的可满足性保留版本，即那些被替换的版本，当移动到公式的头部时将成为存在量词。

为了让生活更简单一些，让我们把否定推向原子。我们还可以看到 w 没有出现在 ¬G(x,x)∨¬H(z) 中，x,z 也没有出现在 H(w) 中，这让我们可以在内部分配量词。

然后我们得到公式∀w¬H(w) ∨ ∃x∀z (G(x,x)∧ H(z)) 。

• 如果我们要反驳公式:

我们对∃x进行skolem化并删除∀w，∀z并获得:

¬H(w) ∨ (G(c,c)∧ H(z))

经过CNF变换后，我们有:

(¬H(w) ∨ G(c,c)) ∧ (¬H(w) ∨ H(z))

两个子句都只有一个正字面量，所以它们都是喇叭子句。翻译成 Prolog 语法我们得到:

g(c,c) :- h(W).
h(Z) :- h(W).

• 如果我们要证明公式:

我们必须在 skolemize 之前取反，导致:

∃w H(w) ∧ ∀x∃z (¬G(x,x) ∨ ¬H(z))

对∃w和∃z进行skolemizing，删除∀x和CNF变换后，我们得到:

H(c) ∧ (¬G(x,x) ∨ ¬H(f(x)))

这可以解释为一个事实 h(c) 和一个查询 ?- g(X,X), h(f(X))。

老实说，这两种变体都没有多大意义 - 第一个变体不会因任何输入而终止，而在第二个版本中，查询将失败，因为 g/2 未定义。