transform first oder logic (FOL) to CNFFormula

Question

This is my problem: I don't know how to transform ∃m : m ∈ N to a CNF Formula. I just understand the formula ∃x(A(x)vB(X)).

Answer 1

I think you could do something like this:

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!

You can try to write a Prolog DGC grammar to automate this process.