Семинар 6

1) Выпишите эквивалентные преобразования для вытягивания кванторов, аналогичные примеру из лекции:

p ∧ (∃x.q) ⇔ ∃y.p ∧ (subst (x ↦ y) q).

2) Постройте предварённые нормальные формы для следующих формул (кванторы в этих обозначениях не являются жадными):

(1) ¬∀x∃y∃z∀u.R(x,y,z,u)
(2) (∀x R(x, y) → (∃y R(y, y) ∨ ∃z R(z, x))
(3) (∃x R(x, y) → (∀y R(y, y) ∨ ∀z R(z, x))
(4) (∀x R(x) → ∀y (R(y) → ∀z R(z)))
(5) (∀x φ(x) ∨ (∃x (φ(x) → ∀y ψ(y))))
(6) (∃x (φ(x) → ψ(x)) → ∀x (ψ(x) → ∃y φ(y)))
(7) ((¬∃x φ(x) ∨ ∀x ψ(x)) ∧ (θ → ∀x η(x)))
(8) ((¬∃x φ(x) ∨ ∀x ψ(x)) ∧ (θ → ∃x η(x)))
(9) ∀x ∃y ((φ(x) → ψ(y, z)) → ∃x ∀z (ψ(x, z) ∧ φ(y)))
(10) (∀x φ(x) → ∀y (∀z ψ(x, z) → ∀u φ(u)))

Проверьте результаты с помощью функции pnf из репозитория с кодом.