logic - 将一阶逻辑 (FOL) 转换为 CNFFormula

Question

这是我的问题：我不知道如何转换∃m : m ∈ N为 CNF 公式。我只是理解公式∃x(A(x)vB(X))。

Answer 1

我认为你可以这样做：

N(x): x is a natural number
S(x): is a specific object that depends on the object x (Skolem function)

∀n[N(n) → ⴺm[N(m) ∧ (m>n)]]                # Skolemize existential quantifiers
≡ ∀n[N(n) → (N(S(n)) ∧ (S(n)>n))]          # Drop universal quantifiers
≡ (N(n) → (N(S(n)) ∧ (S(n)>n)))            # Eliminate implication: (α→β) ≡ (¬α∨β)
≡ (¬N(n) ∨ (N(S(n)) ∧ (S(n)>n)))           # Distribute disjunction: α∨(β∧γ)≡(α∨β)∧(α∨γ)
≡ (¬N(n) ∨ N(S(n))) ∧ (¬N(n) ∨ (S(n)>n))   # Conjunctive Normal Form!

您可以尝试编写 Prolog DGC 语法来自动执行此过程。