Повна версія

Головна arrow Природознавство arrow ІНТЕЛЕКТУАЛЬНІ СИСТЕМИ

  • Увеличить шрифт
  • Уменьшить шрифт


<<   ЗМІСТ   >>

ОБЧИСЛЕННЯ ПРЕДИКАТІВ

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

У разі мови логіки предикатів наш алфавіт буде складатися з наступних груп символів:

  • 1) рахунковий список предметних змінних xi, X2, ...;
  • 2) рахунковий список предметних констант <4,02,.;
  • 3) рахунковий список функціональних символів / 1, / 2, • • •;
  • 4) рахунковий список предикатних символів Р , Р 2 > ...;
  • 5) логічні константи І, Л;
  • 6) логічні зв'язки V, &, - ?, «->;
  • 7) квантори V і 3;
  • 8) дужки і ( і , н ) "і кома і ," •

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

Правильні вирази мови логіки предикатів розбиваються на два непересічних безлічі - безліч термів і безліч формул. Дамо спочатку індуктивне визначення безлічі термів.

Т1) однобуквеним слово, що складається з предметної змінної якої предметної константи, є терм.

Т2) Якщо $ 1, ..., f n - терми і д - функціональний символ арності п, то слово g (t 1, ..., t n ) - є терм.

Індуктивне визначення формул логіки предикатів спирається на вже введене поняття терма.

Ф1) однобуквеним слово складається з логічної константи І або Л, є формула логіки предикатів.

Ф2) Якщо? 1, ..., t n - терми і g - предикатний символ арності п, то слово g (tu ..., t n ) є формула логіки предикатів.

ФЗ) Якщо / і g - формули логіки предикатів, то слова (- * /). (/ V g), (f & g), (/ - » д), (/ <-> д) суть формули логіки предикатів (такі формули будемо називати атомарними або атомами).

Ф4) Якщо / - формула логіки предикатів їх - предметна змінна, то слова (Vx /) і (3х /) суть формули логіки предикатів.

Інтерпретацією мови логіки предикатів називаємо четвірку (М, F, Fi, F 3 ), таку що:

  • а) М - непорожня множина, зване областю інтерпретації;
  • б) F { - функція, що зіставляє кожній предметній константі деякий елемент із М;
  • в) F 2 - функція, що зіставляє кожному функціональному символу / арності п деяку n-місцеву функцію, певну на М і приймаючу значення з М.
  • г) F 3 - функція, що зіставляє кожному предикатні символу Р арності п деякої n-місцевий предикат певний на М (функцію зі значеннями І, Л).

Якщо задана інтерпретація I = (М, F , F 3 , F 3 ), то кожен терм t мови логіки предикатів визначає в цій інтерпретації деякуфункцію (4) /, певну на М і приймаючу значення з М, а кожна формула / - предикат (/) /, певний на М (в вироджених випадках (?) / може ототожнюватися з елементом М, а (/) / с логічної константою).

Тут використовується наступне індуктивне визначення:

  • 1) Якщо х - предметна змінна, то (х) / є тотожна функція від змінної х певна на М.
  • 2) Якщо а - предметна константа, то (а); є елемент Fj (а) з М.
  • 3) Якщо для термів ty , ..., t n вже визначені ..., ( t n ) j , / - функціональний символ арності п і ф = Рг (/) - функція від п змінних, що відображає М п в М, то

4) (І), = І, (Л); = Л.

  • 5) Якщо для термів t, ..., t n вже визначені (ti) /, ..., (< ") /, Р - предикатний символ арності п і = F 3 (P) - предикат від п змінних , що відображає М "в (І, Л), то
  • 6) Якщо для / ід вже визначені (/) / і ( /) /,

(/ V p) / i (/ & #) /, (/ ff) /, (/ < "*

істиннісних функцій для ->, V, &, ->, <-> до (/) / і (<;) /.

7) Якщо вже визначено предикат (/) / = (xj, ..., х п ), то (Vx, /) / = i /> (xi, ..., Xi_i, Xi + i, ..., x n ) - предикат, що приймає значення І на таких наборах e * i, ..., aj_i, aj + i, ..., a n елементів Л /, що для кожного at з М значення ф (а i, .. ., a n ) є І. Аналогічно, (3xj /) / =? (х ь ..., x 4 _i, * j + i, ..., х ") - предикат, що приймає значення І на таких наборах aj, ..., aj_i, aj + i, ..., o n елементів М, що існує а * з М, що значення ф (ос , ..., а ") є І.

Входження змінної х в формулу / логіки предикатів, розташоване всередині подформул виду (Vxp) або (ЗХД), називається зв'язаним, входження змінних не є пов'язаними, називаються вільними. Мінлива має хоча б одне вільне входження в формулу або терм /, називається вільної змінної /. Як неважко бачити, функція або предикат (/) /, певна вище, залежить лише від вільних змінних /. Формула без вільних змінних називається замкнутою.

У формулі 3xi ((Vx2 / 'i (x2, xi)) vP2 (^ 2.a ; i)) перше входження змінної ХГ пов'язане, а друге - вільний, обидва входження змінної Xj пов'язані. Тим самим, у цієї формули одна вільна змінна - хг- Формула ((3xiPi (xi)) - "(УГГ-Рг ^ г))) - приклад замкнутої формули.

Терм t називається вільним для змінної Xi у формулі логіки предикатів /, якщо ніяке вільне входження х * в / не лежить в області дії ніякого квантора Qxj, де Q 6 {V, 3}, Xj - змінна, що входить в терм t.

Наприклад, терм / (xj, хз) вільний для х у формулі

але не вільний для xj у формулі

Якщо / - є формула логіки предикатів, х - вільна предметна змінна формули / і t - терм, то через Sf /

позначимо результат підстановки в / терма t замість всіх вільних входжень змінної х.

Лемма 15 (про інтерпретації). Якщо / - є формула логіки предикатів, х - вільна предметна змінна формули / і t - терм, вільний для змінної х в}, то для будь-якої інтерпретації I формула (Sff) j визначає предикат, що виходить підстановкою в (/) / функції (t ) / замість змінної х.

Доказ цієї леми може отримано індукцією по побудові формули / і рекомендується в якості самостійного вправи.

Якщо формула / визначає в інтерпретації / предикат, тотожне рівний І, то вона називається істинної в I, a. I в цьому випадку називається моделлю для /.

Формулу логіки предикатів / називаємо загальнозначущої, якщо вона істинна у всіх інтерпретаціях, і здійсненним, якщо хоча б в одній інтерпретації вона визначає не тотожне помилковий предикат.

Якщо формула Д & ... & / "-> / о общезначима, то / о називається логічним наслідком формул / ь • • •, / п , якщо формула h <- * / 2 общезначима, то формули f і / 2 називаються еквівалентними .

Формула ((-'Pi (xi)) V Pi (xi)) є приклад загальнозначущої формули. Формула ((-> Pi (ii)) V Pi (fi (xi))) - здійсненна, але не общезначима.

Далі, як і в випадку логіки висловлювань, домовимося опускати дужки, маючи на увазі, що -> - пріоритетна операція, і в разі, коли порядок розставляння дужок не суттєвий (наприклад, для асоціативних операцій). Крім того, домовимося опускати дужки в формулах виду (QiiQiA)), де Q, Qz - будь-які квантори. Наприклад, замість

писатимемо ^ хЗх'р 1 х 3 Р (xi, X 2 , x 3 ).

Для вказівки дедуктивної системи, що перераховує всі загальнозначущі формули логіки предикатів, скористаємося наявними у нас схемами аксіом А1) -А3), в яких тепер /, <7, h - довільні формули логіки предикатів, і додамо до них наступні дві схеми аксіом:

А4) Якщо /, д - формули логіки предикатів їх - предметна змінна, яка не є вільною змінною формули /, то формула (Vx (/ - » д)) -? (/ -» (Vx #)) є аксіома.

А5) Якщо / - є формула логіки предикатів, х - предметна змінна і t - терм, вільний для змінної х в /, то формула (Vx /) - "S * / є аксіома.

Правилами виведення в цій дедуктивної системі є вже відоме нам правило modus ponens, а також нове правило (відоме як правило узагальнення ), що дозволяє з формули / виводити формулу (Vx /). Як і в випадку логіки висловлювань, обмежуємося лише логічними зв'язками - »і причому з кванторів використовуємо тільки квантор спільності. Легко бачити, що квантор існування може бути виражений через квантор спільності і заперечення: формули З х Л (х) і _, (Vx ( " , A (x))) еквівалентні.

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

Теорема 21 (Геделя про повноту числення предикатів).

Кожна загальнозначуща формула логіки предикатів є виведеної в наведеній вище дедуктивної системі.

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

З іншого боку, на відміну від логіки висловлювань, для логіки предикатів справедливим є твердження.

Теорема 22 (Черч). Для логіки предикатів не існує алгоритму, що розпізнає загальнозначущі формули.

Доведення теореми Геделя про повноту ми тут не наводимо, оскільки воно близьке за своєю техніці до приводиться нижче доказу повноти процедури автоматичного доведення теорем, що використовує правило резолюції. По завершенні останнього ми повернемося до теоремі Геделя і дамо короткий нарис схеми її докази.

 
<<   ЗМІСТ   >>