单独的 EXISTS 子句的 skolemization 是如何工作的?

发布于 07-21 19:21 字数 317 浏览 12 评论 0原文

如果我有一个像这样的公式:

FAx FAy (Ez(!A(x,z) v !A(y,z)) v B(x,y))

(FA = For All / E = Exists)

skolemization 的规则是这样的:

  1. 如果 E 在 FA 外部,则替换为常量,或者
  2. 如果 E 在 FA 内部,则替换为包含来自外部的所有变量的新函数FA 作为论据。

那么在这种情况下我该怎么办呢? 我可以删除 Exists 量词还是用常量替换它?

谢谢!

If I have a formula like:

FAx FAy (Ez(!A(x,z) v !A(y,z)) v B(x,y))

(FA = For All / E = Exists)

The rules of skolemisation say that:

  1. if E is outside FA replace with a constant or
  2. if E is inside FA replace by a new function contain all the vars from outside the FA as arguments.

So what do I do in this case? Can I just drop the Exists quantifier or do I replace it with a constant?

Thanks!

如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(1

旧时模样2024-07-28 19:21:41

首先使用标准符号来写:

∀x∀y(∃z(!A(x,z)∨!A(y,z))∨B(x,y))

现在,应用第二个 skolemization 规则:

∀x∀y((!A(x,f(x,y))∨!A(y,f(x,y)))∨B(x,y))

所以我用包含来自外部的所有变量的函数替换了 ∃z 。

现在,这仍然不是 Skolem 范式,因为它不是合取 prenex 范式:公式仍然使用大量析取 (∨)。 删除这些由您决定。

First write this using standard notation:

∀x∀y(∃z(!A(x,z)∨!A(y,z))∨B(x,y))

Now, applying your second skolemisation rule:

∀x∀y((!A(x,f(x,y))∨!A(y,f(x,y)))∨B(x,y))

So I've replaced ∃z with a function containing all vars from outside.

Now, this still isn't in Skolem normal form, because it isn't in conjuctive prenex normal form: the formulas still uses lots of disjunctions (∨). Removing those is left up to you.

~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文