28. Теорема Ембрана. Метод спростування Ембрана.

Теорема 9.2.2 (Ербран, дуальна форма). Пренексна формула Q M( ) всюди істинна Û існують системи термів ,…, , …,  ,…, ербранівського універсу сколемівської формули $у₁…$у_nF, де F – це формула M (g₁( ), …, g_m( ), y₁, …, y_n), такі, що формула [ ,…, ]Ú…Ú [ ,…, ] – тавтологія.

На теоремі Ербрана базується метод спростування Ербрана.

Маємо FÛY_(де _Y – замикання _F) _ÛØYсуперечність Û існує ербранівська розгортка, що є суперечністю.

28. Поняття уніфікатора. Метод резолюцій для логік 1-го порядку.

Підстановка a називається уніфікатором для множини термів {t₁, …, t_n}, якщо a(t₁) = a(t₂) =…= a(t_n). У цьому випадку кажуть, що множина термів {t₁, …, t_n} уніфікується підстановкою a.

Множина термів уніфікується, якщо для неї існує уніфікатор.

Уніфікатор u – найзагальніший уніфікатор (НЗУ) множини термів {t₁, …, t_n}, якщо для кожного уніфікатора a цієї множини існує підстановка h така, що a = u*h.

В загальному вигляді правило резолюцій має два диз'юнкти-засновки та один диз'юнкт-висновок – резольвенту засновків.

Диз'юнкт D – резольвента диз'юнктів D₁ та D₂, якщо D є однією з бінарних резольвент:

1) D₁ та D₂;

2) D₁ та склеювання чи прикладу D₂;

3) склеювання чи прикладу _D_1 та D₂;

4) склеювання чи прикладу D_1 та склеювання чи прикладу _D₂.

Приклад 9.2.9. Нехай маємо диз'юнкт D = p(x)Ú p(g(y))ÚØq(x). Його літери p(x) та p(g(y)) мають НЗУ u = [xag(y)]. Диз'юнкт u(D) = p(g(y))ÚØq(g(y)) – склеювання диз'юнкта _D.

28. Секвенційне числення класичних логік 1-го порядку.(1й модуль)

29. Секвенційні числення логік еквітонних предикатів.(Ааааааа!капец тупой вопрос! Аааааааа!)

базові секвенційні форми:

_-Ø _-Ø

_-Ú _-Ú

_-RT _-RT

_-RR _-RR

_-RØ _-RØ

_-RÚ _-RÚ

Теорема 8.1.1. Нехай S = _L_K, U = _C _Z, W = _G_D, нехай та  секвенційні форми. Тоді:

1) якщо L K, то G D;

2) якщо L K та C Z , то G D.

При побудові секвенційного дерева можливі такі випадки:

1) процедура завершена позитивно, отримане скінченне замкнене секвенційне дерево;

2) процедура завершена негативно, отримане скінченне незамкнене дерево;

3) процедура не завершується, і тоді маємо нескінченне секвенційне дерево.

28. Коректність та повнота секвенційних числень. Наслідки теореми повноти.

Теорема 8.1.2 (коректності). Нехай секвенція _G_D вивідна. Тоді GD.

Теорема 8.1.4 (повноти). Нехай G D. Тоді секвенція _G_D вивідна.

28. Інтерполяційна теорема. Семантична та синтаксична визначеність. Теореми про визначеність.

Специфіковану символами _ чи _ формулу для стислості називатимемо s-формулою.

Секвенція  примітивно замкнена, якщо існує примітивна формула  така: _ та _.

Теорема 9.6.4 (інтерполяційна теорема). Нехай секвенція _ має виведення. Тоді існує формула  сигнатури ()()() така, що секвенції _ та _ мають виведення.

Таку  називають інтерполяційною формулою, або інтерполянтом.

При ()() =  твердження теореми може бути невірним

Предикатний символ q семантично визначний через предикатні символи {p₁,…, p_n}, де q{p₁,…, p_n}, якщо для кожних {p₁,…, p_n}-тотожних еквітонних моделей істинності A=(M, I_A) та В=(M, I_В) множини формул  маємо q_A  q_В .

Предикатний символ q синтаксично визначний через предикатні символи {p₁,…, p_n} в множині формул , якщо існує формула  із () ={p₁,…, p_n} така, що   q.

Теорема 9.6.6. Нехай ПС q синтаксично визначний через {p₁,…, p_n} в множині формул . Тоді q семантично визначний через {p₁,…, p_n}.

Теорема 9.6.7. Нехай предикатний символ q семантично визначний через {p₁,…, p_n}. Тоді q синтаксично визначний через {p₁,…, p_n} в множині формул .