Задачі для самостійного розв’язування

1. Довести, що

а) ├ [TEX]\forall [/TEX]x [TEX]\forall [/TEX]y А → [TEX]\forall [/TEX]y [TEX]\forall [/TEX]x А;

б) ├ [TEX]\forall [/TEX]x (А → В) → ([TEX]\forall [/TEX]x А → [TEX]\forall [/TEX]x В).

2. Довести, якщо терм і вільний для змінної х у формулі А (х), то:

а) [TEX]\forall [/TEX]x А (х) ├ А (t);

б) А (t) ├ [TEX]\exists [/TEX]x А (х).

3. Довести, що для будь-яких форм  л А і В:

а) А, В ├ А [TEX]\wedge [/TEX] В;

б) А → С, В → D, ¬ А → В ├ ¬ С → D;

в) ├ А [TEX]\vee [/TEX] В ~ ¬ (¬ А [TEX]\wedge [/TEX] ¬ В).

4. Звести до ВНФ такі вирази:

а) ¬ [TEX]\forall [/TEX]y [TEX]\exists [/TEX]x (А(х) → В(у));

б) [TEX]\exists [/TEX]x [TEX]\forall [/TEX]y В(х, у) ⇔ [TEX]\exists [/TEX]x А(х);

в) [TEX]\forall [/TEX]x А(х) → ¬ ([TEX]\forall [/TEX] x (В(у) [TEX]\vee [/TEX]  [TEX]\forall [/TEX]y С(х, у)).

5. Задані формули:

а) (¬ Р [TEX]\wedge [/TEX] Q) → ¬ R; б) (Р [TEX]\wedge [/TEX] (R → ¬ Q)) → S; в) ¬ (¬ Р [TEX]\vee [/TEX] ¬ Q) → (¬ R [TEX]\vee [/TEX] S);

перетворити у КНФ.

6. Істинність заданих предикатних клауз довести методом ідентифікації:

а) [TEX]\exists [/TEX]x [TEX]\forall [/TEX]y Р(х, у) → [TEX]\forall [/TEX]v [TEX]\forall [/TEX]u Р(и, v), [TEX]\exists [/TEX]x [TEX]\forall [/TEX]v P(x, v) → [TEX]\forall [/TEX]х [TEX]\forall [/TEX]y P(x, y);

б) [TEX]\exists [/TEX]x [TEX]\forall [/TEX]y Р(х, у) → [TEX]\forall [/TEX]u [TEX]\forall [/TEX]v Р(v, u), [TEX]\forall [/TEX]х [TEX]\forall [/TEX]v P(x, v) → [TEX]\exists [/TEX]y [TEX]\exists [/TEX]u P(y, u), ¬ [TEX]\exists [/TEX]v [TEX]\exists [/TEX]x P(x, v) → ¬ [TEX]\exists [/TEX]y [TEX]\forall [/TEX]х P(x, y);

в) [TEX]\forall [/TEX]х [TEX]\forall [/TEX]y Р(х, у) → [TEX]\exists [/TEX]x [TEX]\forall [/TEX]y Q(x, y), [TEX]\exists [/TEX]x [TEX]\exists [/TEX]y ¬ R(x, y) → [TEX]\exists [/TEX]x [TEX]\forall [/TEX]y ¬Q(x, y), [TEX]\exists [/TEX]x [TEX]\exists [/TEX]y ¬R(x, y) → [TEX]\forall [/TEX]х [TEX]\forall [/TEX]y ¬ P(x, y).

7. Довести істинність предикатних клауз методом резолюцій:

а) [[TEX]\forall [/TEX]x [TEX]\forall [/TEX]y P(x, y) → [TEX]\exists [/TEX]x Q(x)] → [[TEX]\exists [/TEX]x ¬ [TEX]\forall [/TEX]y P(x, y)[TEX]\wedge [/TEX] [TEX]\exists [/TEX]x [TEX]\exists [/TEX]y P(x, y)]  →¬ [TEX]\exists [/TEX]x [TEX]\exists [/TEX]y ¬ P(x, y) [TEX]\vee [/TEX] ¬ [TEX]\forall [/TEX]x [TEX]\forall [/TEX]y ¬ P(x, y);

б)[TEX]\exists [/TEX]x Р(х, у) → ¬ [TEX]\exists [/TEX]y ¬ Р(х, у) → [TEX]\forall [/TEX]x [TEX]\exists [/TEX]y Q(x, y), [TEX]\forall [/TEX]y P(x, y) → ¬ [TEX]\forall [/TEX]y ¬ P(x, y), [TEX]\forall [/TEX]y P(x, y) → ¬ [TEX]\exists [/TEX]x ¬ P(x, y) → [TEX]\forall [/TEX]y [TEX]\exists [/TEX]x Q(x, y);

в) [TEX]\exists [/TEX]x [TEX]\exists [/TEX]y Р(х, у), [TEX]\forall [/TEX]x [TEX]\exists [/TEX]y Р(х, у) → [TEX]\exists [/TEX]y Q(y),

[TEX]\forall [/TEX]x Q(x) [TEX]\vee [/TEX][[TEX]\exists [/TEX]y [TEX]\exists [/TEX]x P(x, y) → ¬ [TEX]\exists [/TEX]x [TEX]\forall [/TEX]y ¬ P(x, y)],

¬[TEX]\exists [/TEX]x ¬ Q(x) → [TEX]\exists [/TEX]x Q(x, y) → ¬ [TEX]\forall [/TEX]y ¬ P(x, y).

Коментарі. У цьому розділі система аксіом і правил виведення взяті з [14,19,20]. Більш детальне викладення цього матеріалу можна знайти в [12,27]. Властивості числення предикатів першого порядку і випереджені нормальні форми випливають з [27], а побудова доведень узята з [1,7,23,26].

 

1