#logic #cnf
#Логические #cnf
Вопрос:
Это моя проблема: я не знаю, как преобразовать ∃m : m ∈ N в формулу CNF. Я просто понимаю формулу ∃x(A(x)vB(X)) .
Комментарии:
1. Тогда это не проблема программирования. Но что-то, что принадлежит mathoverflow.net
2. В нем говорится, что для всех n, где n — натуральное число, такое, что существует m, которое является натуральным числом, и m также больше n. Так что, возможно, напишите программу prolog, которая это докажет. проверка (N,M)
3. Так это проблема в арифметике Пеано?
4. спасибо, Рима, я думаю, что вы правы, и, возможно, мне следует преобразовать последовательность в формулу соединения
Ответ №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 для автоматизации этого процесса.