На головну

логіці предикатів

  1.  Алфавіт логіки предикатів.
  2.  Алфавіт мови логіки предикатів
  3.  Здійснимість і общезначімость формул логіки предикатів. Теорема Черча.
  4.  Імплікація і еквіваленція предикатів, їх області визначення.
  5.  ІСТОРІЯ про собачу ЛОГІКА
  6.  Кон'юнкція і диз'юнкція предикатів, їх безлічі істинності.

До додатком До змісту До титулу

Лекція 6. Особливості методу резолюцій при доказі теорем в

логіці предикатів

1. Основні поняття.

Ідея Робінсона - автора методу резолюцій, - полягає в тому, щоб в логіці предикатів можна було, працювати, безпосередньо, з диз'юнкт, що містять змінні, не вдаючись до попередньої заміни змінних константами з області визначення  . Ця ідея забезпечується використанням операцій підстановки та уніфікації. Щоб визначити суть цих операцій, введемо кілька нових понять і визначень.

поняття «вираз». Під виразом розуміється терм, безліч термів, безліч атомів, літера, диз'юнкт, безліч диз'юнктів. Коли в вираженні невідомі ніякі змінні, воно називається основним виразом: основний атом, основна літера, основний диз'юнкт, основний терм, що говорить про відсутність в них змінних.

поняття «підстановка». Попередньо на прикладі з'ясуємо, в чому полягає проблема пошуку контрарних пар в логіці предикатів. Розглянемо наступні диз'юнкт:

Поки немає ніякої літери в  , Контрарной який-небудь літері в  . Однак, підставивши в  функцію  замість змінної  , Отримаємо:

тепер літера в  контрарності літері в .

Отже, можна отримати резольвенту з и :

Визначення 1: підстановка - Це кінцеве безліч виду  , Де кожна  - Це змінна, кожен  - Терм, що відрізняється від  , а все  - Різні.

 Визначення 2: Нехай  - Підстановка, а  - Вираз. тоді  - Це вираз, отримане з  заміною одночасно всіх входжень змінної  в вираженні  на терм .  називається прикладом  . Наприклад, нехай и  Тоді підстановка дає приклад

поняття «композиція підстановок». Нехай дано підстановки и  тоді композиція и  є підстановка  , Яка виходить з безлічі  викреслюванням усіх елементів  , для яких  і всіх елементів  таких, що  . Розглянемо приклад визначення композиції підстановок и  . тоді  Однак за визначенням  повинна бути викреслена; и  також повинні бути викреслені, так як и  містяться серед змінних підстановки  . В результаті отримуємо

поняття «уніфікатор для безлічі виразів». підстановка  називається уніфікатором для безлічі виразів  тоді і тільки тоді, коли  . Вважається, що безліч виразів уніфікуючих, якщо для нього існує уніфікатор.

уніфікатор  для безлічі виразів  називається найбільш загальним уніфікатором (НОУ) тоді і тільки тоді, коли для кожного уніфікатора  для цього безлічі існує Токаю підстановка  , що  . Нехай, наприклад, є безліч виразів  . тоді  є найбільш загальний уніфікатор для  , а  є уніфікатор.

Опишемо по кроках алгоритм уніфікації, Який знаходить НОУ, якщо безліч  уніфікуючих, і повідомляє про невдачу, якщо це не так [6]:

1) Встановити и  , де  - Порожня підстановка, яка не містить елементів. Перейти до кроку 2.

2) Якщо  не є одноелементна безліччю, то перейти до кроку 3. В іншому випадку покласти  і закінчити роботу.

3) Кожна з літер в  розглядається як ланцюжок символів і виділяються перші подвираженія літер, які не є однаковими у всіх елементів  , Тобто утворюється так зване безліч неузгодженостей типу  . Якщо в цій множині  - Змінна, а  - Терм, відмінний від  , То перейти до кроку 4. В іншому випадку закінчити роботу з висновком:  НЕ уніфікуючих.

4) Нехай и

5) Встановити  і перейти до кроку 2.

Розглянемо роботу алгоритму знаходження НОУ для безлічі  Кроки наступні:

1) и

2) Так як  не є одноелементна безліччю, то перейти до кроку 3.

3) Безліч неузгодженостей  тобто заміна

4)

5) Так як безліч  знову не одноелементні, то безліч неузгодженостей буде  тобто заміна .

6)

7) Маємо  , Тобто .

8)

Так як отримано одноелементні безліч, то шуканий найбільш загальний уніфікатор .

Можна показати, що алгоритм уніфікації завжди завершується на етапі 2, якщо безліч  уніфікуючих, і на кроці 3 - в іншому випадку.

поняття «склейка диз'юнкт ». Якщо дві або більше літер (з однаковим знаком) диз'юнкт  мають найбільш загальний уніфікатор  , то  називається склеюванням  . якщо  - Одиничний диз'юнкт, то склейка називається одиничною склеюванням.

 Приклад: Нехай

 Тоді перша і друга літери мають найбільш загальний уніфікатор  . отже,  є склейка .

 поняття «бінарна резольвента». нехай и  - Два диз'юнкт (звані диз'юнкт-посилками), які не мають жодних спільних змінних. нехай також и  - Дві літери відповідно в и  . якщо и  мають найбільш загальний уніфікатор  , То диз'юнкт  називається бінарною резольвенти и  , А літери и  називаються відрізати літерами.

 Приклад: Нехай и  Так як змінна  входить в и  , То замінимо змінну в  на  , Тобто  вибираємо и  Так як  , то и  мають найбільш загальний уніфікатор .

отже,

 Таким чином,  - Бінарна резольвента и  , а и  - Відрізані літери.

поняття «резольвента логіки першого порядку». Резольвенти диз'юнктів-посилок и  є одна з наступних резольвент:

1) бінарна резольвента и ;

2) бінарна резольвента  і склейки

3) бінарна резольвента  і склейки

4) бінарна резольвента склейки  і склейки

 Приклад: Нехай ,

 Тоді склейка диз'юнкт  є  і резольвенти для и  буде



© um.co.ua - учбові матеріали та реферати