gpt4 book ai didi

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

转载 作者:行者123 更新时间:2023-12-01 22:09:56 25 4
gpt4 key购买 nike

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

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

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

最佳答案

我将始终使用 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 未定义。

关于prolog - 如何写成 skolem 形式?(Prolog),我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/48634301/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com