Семантичні дерева
Обчислення семантичних дерев схоже на обчислення по Бету.
Нехай - пропозиція, і S - відповідна множина диз'юнктів. Якщо здійсненно, то воно є істинним у деякій ербранівській інтерпретації. Відповідно, всі основні приклади диз'юнктів з S істинні у цій інтерпретації. Отже, якщо пропозиція нездійсненна, будь-яка спроба підтвердити всі основні приклади диз'юнктів S за допомогою означення основних атомів r (t1,…, tn), де терми t1,…, tn належать ербранівському універсуму, приречена на невдачу. Цей факт може бути виявлений за кінцеве число кроків шляхом побудови кінцевої множини нездійсненних в ербранівській інтерпретації основних прикладів. Згідно з теоремою Ербрана ці основні приклади нездійсненні у всіх інтерпретаціях.
Отже, питання про те, як побудувати процедуру, яка, маючи на вході пропозицію та відповідну множину диз'юнктів,
якщо нездійсненно, зупиняється після кінцевого числа кроків, видаючи кінцеву множину основних прикладів;
якщо здійсненно, процедура, у загальному випадку, не дає жодної відповіді за кінцевий час, при цьому вона здійснює побудову ербранівської інтерпретації, на якій істинно .
Тобто. за допомогою цієї процедури ми хочемо отримати доказ нездійсненності пропозиції чи контрприкладу. При побудові такої процедури застосовуються семантичні дерева.
Деревом називається зв'язковий граф без циклів, одна з вершин якого (єдина) називається коренем. З кореня може бути досягнута будь-яка вершина дерева. Дві вершини дерева, пов'язані ребром (гілкою) знаходяться щодо попередження. T=(x, r) - дерево, xry означає: x є безпосереднім попередником y, а y – послідовником x. Тут x, y -елементи з багатьох основнихприкладів із запереченням чи без.
Нехай S = 1, ..., Cn - безліч диз'юнктів; P1, ..., Pl - атоми, що входять в диз'юнкти множини S, 1, ..., an,, ... - Ербрановський універсум множини S.
Семантичним деревом для S називається дерево Т, яке задовольняє наступним умовам:
Коренем дерева є довільна точка. Вершини, відмінні від кореня, є основними прикладами атомів P1,…,Plна ербранівському універсумі 1,…,an,…> . Кожна вершина має дві наступні вершини, саме Pi(ai1,…,aik) иP(ai1,…,aik).
Кожна гілка дерева Т, містить основні приклади Pi1(al1,…alk),…,Piq(aq1,…,aqk) представляє кон'юнкцію цих основних прикладів.
Диз'юнкція всіх кон'юнкцій гілок дерева є загальнозначущою формулою.
Якщо вершина дерева Т має вигляд P(ai1,…,aik), то ні на якій галузі дерева, що проходить через цю вершину, не може зустрітися P(ai1,…,aik).
Якщо при побудові дерева Т отримана вершина k, яка вступає в суперечність з яким-небудь основним прикладом одного з диз'юнктів C1, Cnмножини S, то вважається заключною вершиною, і про відповідну гілки говорять, що вона суперечлива.
Практично побудова семантичного дерева множини S починається з P1(a11,…,a1k):
Якщо один із диз'юнктів множини S містить P(ai1,…,aik), то права гілка суперечлива,
P(ai1,…,aik) є заключною вершиною, і побудова триває лівою гілкою.
Припустимо, що P(ai1,…,aik) – не остання вершина. Тоді з неї виходить дві гілки до двох вершин дерева, що означає будь-який інший атом пропозиції, що ще не зустрічався в цій галузі, і його заперечення. Мета побудови: досягти заключної вершини, вичерпавши всі атоми S.
Безліч диз'юнктів S називаєтьсясептичним семантичним деревом, якщо існує семантичне дерево для S, гілки якого суперечливі.
Гілка семантичного дерева множини диз'юнктів S називаєтьсяповною, якщо для всіх основних прикладів P(ai,…,an) кожного атома Р у цій галузі містяться P(ai,…,an) або
приклад. Нехай дано пропозицію : x[P(x)&(P(x)Q(f(x)))&Q(f(x))]. Тоді
Семантичне дерево Т для S зображено малюнку 5.
Символ означає протиріччя. Праворуч від нього вказано номер диз'юнкту, відповідального за це протиріччя. Подивимося, чому друга гілка суперечлива. Ця гілка представляє кон'юнкцію
Другий диз'юнкт множини має вигляд. Тому ми вимагаємо, щоб формула P(x)Q(f(x)) була істинною для кожного х. Гілка 2 стверджує, що в ербранівському універсумі існує значення змінної х, що дорівнює а, для якого виконується
Звідси ми також маємо Q(f(a))&P(a) =(Q(f(a))P(a)). Отже, розглянута гілка дає протиріччя з другим диз'юнктом множини.
Порядок вибору чергового елемента Н для підстановки в атоми з безлічі Sдовільний.
Якщо безліч диз'юнктівSнеможливо, тоSзаперечується семантичним деревом.
Фактично теорема Ербрана надає можливість під час перевірки здійсненності пропозиції або безлічі диз'юнктів S використовувати методи логіки висловлювань, наприклад, метод семантичних таблиць або метод резолюцій. Якщо S неможливе, то існує безліч основних прикладів диз'юнктів множини S, яке також буде нездійсненним. Ця кінцева множина складається з висловлювань PL, і його нездійсненність може бути виявлена відомими методами. Таким чином, для кожної множини диз'юнктів Sми перераху-
">