3

(∀u∃va(u,v)) ∧ (∀x∃ya(x,y)) のスコーレム化された形式は?

さまざまな perenex 正規形が考えられるため、よくわかりません。

  • ∀u∃v ∀x∃y (a(u,v) ∧ a(x,y))
  • ∀u∀x ∃v∃y (a(u,v) ∧ a(x,y))
  • …</li>

異なる skolemized 形式が続きます。

  • ∀u ∀x (a(u,f(u)) ∧ a(x,g(u,x)))
  • ∀u∀x (a(u,f(u,x)) ∧ a(x,g(u,x)))

私の考えでは、それらは互いに同等ではありません。それとも私はここで間違っていますか？

4

1 に答える 1

2

はい、前置正規形は特定の FO 式に対して一意ではありません。したがって、Skolemization も一意ではありません。同じ「スコープエスケープ」のより簡単な例は、式 ∃xAx → ∃yBy であり、接頭辞は ∀x∃y (Ax → By) および ∃y∀x (Ax → By) であり、それぞれのスコーレム化 ∀x (¬ Ax ∨ Bf(x)) および ∀x (¬ Ax ∨ B a)、aa 定数。

さて、適切な質問は、これらの式の非同等性が特定の問題にとって重要かどうかです。そうであれば、おそらく Skolemization は最適なツールではありません。Skolemization は、式の充足可能性を維持するために設計されたプロセスですが、等価性を犠牲にすることもあります。

(そして、いずれにせよ、上記の例だけであるとしても、単一の式の個別のスコーレム化がなぜ等充足可能であるかを確認することは良い練習になります)

于 2011-12-27T11:45:56.977 に答える