单独的 EXISTS 子句的 skolemization 是如何工作的?
如果我有一个像这样的公式:
FAx FAy (Ez(!A(x,z) v !A(y,z)) v B(x,y))
(FA = For All / E = Exists)
skolemization 的规则是这样的:
- 如果 E 在 FA 外部,则替换为常量,或者
- 如果 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:
- if E is outside FA replace with a constant or
- 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!
首先使用标准符号来写:
现在,应用第二个 skolemization 规则:
所以我用包含来自外部的所有变量的函数替换了 ∃z 。
现在,这仍然不是 Skolem 范式,因为它不是合取 prenex 范式:公式仍然使用大量析取 (∨)。 删除这些由您决定。
First write this using standard notation:
Now, applying your second skolemisation rule:
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.