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

Виявленню розв'язних і нерозв'язних проблем у самих різних математичних ситуаціях присвячено багато досліджень.

6. Дані і знання. Логіка висловлень (ЛВ) в представленні знань

1. Логіка висловлень (пропозиційна логіка) [1] - одна з базових теорій математичної логіки, на якій базуються більш складні формальні логіки.

Алфавіт логіки висловлень (ЛВ) складається зі зчисленної множини елементарних висловлень, які позначуються літерами (можливо, з індексами) і 5 логічних операцій: заперечення (^), кон'юнкції (/\, або &), диз'юнкції (\/), імплікації (->) і тотожності, еквівалетності (<->), які задаються скінченими таблицями істинності.

Як відомо, кожне висловлення може мати значення істинно (позначається Т, 1), або хибно (позначається F, 0).

Алфавіт висловлень дає змогу будувати складні висловлення (формулу) із простіших за допомогою логічних операцій [1] по наступній рекурсивній схемі, а саме, формулами ЛВ є тільки наступні конструкції:

- кожне висловлення є формулою;

- якщо А і В є формули, то ^A, (A/\B), (A\/B), (A -> B) i (Aя2=я0B) - є формулами.

Формули задають синтаксис мови ЛВ. А який сенс, семантика цієї мови?

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

Літера, або літерал - це елементарне висловлення р або його заперечення ^p. Літери р і ^р є протилежні.

Формула ЛВ називається виконуваною, якщо вона допускає деяку модель, тобто її можна інтерпретувати із значенням Т.

Формула ЛВ А називається суперечністю (не виконуваною), якщо А = F для всіх моделей А (наприклад, (р/\^p).

Формула ЛВ називається тавтологією, якщо вона істина при всіх інтерпретаціях (на всіх моделях). Відмітимо, що заперечення тавтології є суперечність.

2. Нехай, Е - множина формул ЛВ. Формула А є наслідком (логічним) з Е (позначення, Е (= А), якщо на всіх моделях, на яких істині всі формули з Е, істина також формула А. Ясно, що тавтологія є наслідком із пустої множини формул ЛВ.

Легко довести [1], що мають місце:

Твердження 1. Нехай, Е = {H1, H2,… Hn} є множиною формул ЛВ.

Формула А є наслідком (логічним) з Е (E (= A) тоді і тільки тоді, коли імплікація:

(H1/\H2/\…/\Hn) -> A

є тавтологією. Прямим наслідком із твердження 1 є

Твердження 2. Нехай, Е = {H1, H2..Hn} є множиною формул ЛВ.

Формула А є наслідком (логічним) з Е тоді і тільки тоді, коли формула

(H1/\H2/\…/\Hn/\^A)

є суперечністю.

Диз'юнктом називається диз'юнкція скінченного числа літералів, тобто формула виду

(L1\/L2\/..\/Lm).

Її часто записують у «скороченому» вигляді як послідовність літералів: {L1., Lm}.Пустий диз'юнкт - єдиний диз'юнкт, що не виконується, і його позначають через Л.

Кон'юктивною нормальною формою (КНФ) називається кон'юнкція скінченої кількості диз'юнктів.

Теорема 1. Довільна формула ЛВ має логічно еквівалентну їй КНФ.

Наступний алгоритм нормалізації формул ЛВ дає доведення теореми 1.

Етап 1. Спочатку замінюємо (А<->В) на ((А->B)/\(B->A)), а потім заміняємо (U->V) на (^U\/V). Це робиться для виключення операцій <-> і ->.

Етап 2. Необхідну кількість раз застосовуються перетворення на основі законів де Моргана:

^(X/\Y) ==> (^X\/^Y), ^(X\/Y) ==> (^X/\^Y).

Символ ==> означає «замінити на». В цій заміні подвійні заперечення елімінуються, тобто

^^X ==> X.

На цій стадії операція заперечення залишається тілки безпосередньо перед висловленнями.

Етап 3. необхідну кількість разів застосовуються правила перетворень, що виведені із законів дистрибутивності:

X \/ (Y /\ Z) ==> (X \/ Y) /\ (X \/ Z)

(X /\ Y) \/ Z ==> (X \/ Z) /\ (Y \/ Z).

Етап 4. Диз'юнкти, що містять протилежні літерали (тобто висловлення і його заперечення), є тавтологіями і можуть бути еліміновані. Також елімінуються повторення літералів у межах одного ж і того диз'юнкта.

Формула, що отримується в кінці четвертого етапу, і є КНФ, яка еквівалентна вихідній формулі ЛВ.

Відмітимо, що диз'юнкт є тавтологією тоді і тільки тоді, коли він містить пару протилежних літералів. КНФ є тавтологією тоді і тільки тоді, коли всі її диз'юнкти - тавтології.

Єдиним не виконуваним диз'юнктом є пустий диз'юнкт Л.

3. Не існує загального ефективного критерію для перевірки виконуваності КНФ. Але існує зручний метод для виявлення не виконуваності множини диз'юнктів. Дійсно, множина диз'юнктів є не виконувані тоді і тілки тоді, коли пустий диз'юнкт Л є логічним наслідком із неї. Таким чином, не виконуваність множини S можна перевірити, породжуючи логічні наслідки з S, поки не отримаємо пустий диз'юнкт. Для цього використовується наступна схема міркувань.

Припустимо, що дві формули (A \/ X) i (B \/ ^X) - істині. Якщо Х також істина, то звідси випливає, що B істина. Навпаки, якщо Х хибна, то А істина, тобто отримується правило

{(A \/ X), (B \/ ^X)} [= A \/ B,

яке можна записати у вигляді

{^X -> A, X -> B} [= A \/ B. Зокрема, якщо Х - висловлення, а A i B - диз'юнкти, то правило називається правилом резолюції.

Твердження 3. Нехай s1 i s2 - диз'юнкти КНФ S. Якщо літерал р входить у s1 і ^p - у s2, то диз'юнкт

r = (s1\{p}) \/ (s2\{^p})

є логічним наслідком КНФ S.

Тут через si\{L} позначається диз'юнкт, що отримується з si вилученням літералу L. Диз'юнкт r називається резольвентою диз'юнктів s1 i s2.

Твердження 4. Нормальні форми S i (S /\ r) еквівалентні.

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

Метод резолюцій

Крок 1. Якщо Л належить S, то КНФ S є суперечністю, і алгоритм зупиняється.

Крок 2. Вибираються довільні L, s1, s2 такі, що літерал L входить в диз'юнкт s1, а ^L входить у s2.

Крок 3. Обчислюється резольвента r.

Крок 4. КНФ S замінюється на КНФ S' = S /\ r, і повертаються на крок 1. Вибираються довільні L, s1, s2 такі, що літерал L входить в диз'юнкт s1, а ^L входить у s2.

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

1. Необхідно побудувати кон'юктивну нормальну форму для формули А логіки висловлень, де

A = (p -> (q -> r)) -> ((p /\ s) -> r).

Використаємо алгоритм із розділу 1.2. Кожна з нижченаведених формул еквівалентна А.

Етап 1 (виключення імплікацій).

(p -> (q -> r)) -> ((p /\ s) -> r),

^ (p -> (q -> r)) \/ ((p /\ s) -> r),

^ (^p \/ (q -> r)) \/ (^(p /\ s) \/ r),

^ (^p \/ (^q \/r)) \/ (^(p /\ s) \/ r),

Етап 2.

(^ ^p /\ ^ (^q \/r)) \/ ((^p \/ ^s) \/ r),

(^ ^p /\ (^ ^q /\ ^r)) \/ ((^p \/ ^s) \/ r),

(p /\ (q /\ ^r)) \/ ((^p \/ ^s) \/ r).

Етап 3.

a) (p \/ ((^p \/ ^s) \/ r)) /\ ((q /\ ^r) \/ \/ ((^p \/ ^s)

\/ r))

b) (p \/ (^p \/ ^s) \/ r)) /\ /\ (q \/ (^p \/ ^s) \/ r) /\

(^r \/ (^p \/ ^s) \/r);

c) (p \/ ^p \/ ^s \/ r) /\ /\ (q \/ ^p \/ ^s \/ r) /\ (^r

\/ ^p \/ ^s \/ r);

d) T /\ (q \/ ^p \/ ^s \/ r) /\ T;

e) (q \/ ^p \/ ^s \/ r).

Ми отримали, що КНФ В = (q \/ ^p \/ ^s \/ r) формули А складається з одного диз'юнкта.

Приклад

2. Необхідно перевірити за допомогою метода резолюцій, чи є КНФ S суперечністю, де

S = {p \/q, p /\ r, ^q \/ ^r, ^p}.

Диз'юнкти зручно перенумерувати. Отримаємо список:

1. p \/q

2. p \/ r

3. ^q \/ ^r

4. ^p

Далі обчислюються резольвенти і додаються до S. У нижченаведеному списку кожний диз'юнкт - резольвента деяких попередніх диз'юнктів. Номера їх наводяться з права від відповідної резольвенти

5. p \/ ^r 1,3

6. q 1,4

7. p \/ ^q 2,3

8. r 2,4

9. p 2,5

10. ^r 3,6

11. ^q 3,8

12. ^r 4,5

13. ^q 4,7

14. Л 4,9

Отримали, що із КНФ S виводиться пустий диз'юнкт Л, тобто S є суперечністю (не виконуваною формулою).

7. Логіка предикатів (ЛП) в представленні знань

(Теорема про нерозв'язність числення предикатів)

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

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

Мається точне поняття доведення твердження числення предикатів, причому твердження доводиться тоді і тільки тоді, коли воно істинно. У 1936 році Черч показав, що доведеність (і, отже, істинність) у численні предикатів нерозв'язна на відміну від більш простого пропозиціонального числення. (Гільберт вважав цей результат самим фундаментальної результатом, що стосується нерозв'язності, у всій математиці.)

Просте доведення нерозв'язності проблеми істинності можна дати з використанням МНР, хоча це вимагає деякого знайомства з численням предикатів. Читачу, що не знайомий з початками логіки предикатів, ми радимо пропустити приведений нижче зразок доведення.

5.1. Теорема. Проблема істинності числення предикатів першого порядку нерозв'язна.

Доведення. (Тим, хто не знайомий з численням предикатів, рекомендується пропустити.)

Нехай Р - деяка програма в стандартному виді, що містить команди I₁,…, I_s, і нехай u=(P) (визначення див. § 2 р. 2). Ми будемо використовувати наступні позначення символів числення предикатів:

O - індивідний символ,

' - символ одномісної функції (значення якої на х дорівнює х'),

R-символ (u+1) - місного відношення,

x₁, x₂,…, x_a, у - символи індивідних змінних.

Далі, для будь-якої команди I_i, можна записати твердження числення предикатів _i, що описує результат виконання команди I_i. При цьому ми використовуємо символ для позначення зв'язки «і» і символ для позначення імплікації. Твердження _i, визначається в такий спосіб:

якщо I_i=Z(n), тo _i, є твердження

x₁ … x_u: R (x₁, …, x_n, …, x_u, i)R (x₁, …, O, …, x_u, i )

якщо I_i=S(n), то _i, є твердження

x₁ … x_u: R (x₁, …, x_n, …, x_u, i)R (x₁, …, x_n, …, x_u, i )

(c) якщо I_i=T (m, n), тo _i, є твердження

x₁ … x_u: R (x₁, …, x_n, …, x_u, i)R (x₁, …, x_m, …, x_u, i)

(d) якщо I_i=J (m, n, q), тo _i, є твердження

x₁ … x_u: R (x₁, …, x_u, i)((x_m = x_n R(x₁, …, x_u, q))(x_m x_n R(x₁, …, x_u, i)))

Нехай тепер для будь-якого а N символ _a позначає твердження.

(₀₁…_s R (a, O,… O, 1))x₁ … x_u R(x_{1, …,} x_u, s+1)

де ₀ є твердження xy((х'=у x=y) xO). (Це гарантує нам, що при будь-якій інтерпретації з т, n

N і m=n випливає, що т=п.)

Твердження R (a, O,…, О, 1) відповідає вихідному стану

а	0	0	…;	наступна команда Ii

а будь-яке твердження R(x₁,…, х_u, s +1) відповідає зупинці (оскільки немає команди I_s+1). Ми покажемо, що

(*) Р (а)_a істинно.

Припустимо спочатку, що Р(а) і що мається структура, у якій твердження _0,…, _s, і R (a, O,…, O, 1) виконуються. За допомогою тверджень _0,…, _s, ми одержуємо, що кожне з тверджень R(r₁,…. r_u, k),

що відповідають послідовним станам обчислення, також виконується. Зрештою ми приходимо до того, що для деяких b₁,…, b_u N виконується твердження про зупинку R(b₁,…, b_u, s+1) і, отже, виконується твердження x₁ …x_u R(x₁,…, x_u, s+1). Таким чином, твердження _a істинно.

Знову, якщо твердження _a істинно, то воно виконується, зокрема, у структурі N, причому предикатний символ R інтерпретується як предикат R_a, для якого

R_a(a_1,…, а_u, k)На деякому етапі обчислення Р (а) у регістрах містяться числа а₁, a₂,…, a_u, 0, 0,…, а наступна команда є I_k.

Тоді твердження _0,…, _s, і R (a, O,…, O, 1) також виконуються в цій структурі, а отже, і твердження x₁ …x_u R(x₁,…, x_u, s+1). Звідси Р(а).

Якщо в якості Р узяти програму, що обчислює функцію _u (x, х), то співвідношення еквівалентності (*) зводить проблему «x W_x» до проблеми « істинно». Звідси випливає, що остання проблема нерозв'язна.

Математична логіка буяє результатами, що стосуються можливості розв'язання і нерозв'язності. Звичайно мова йде про задачі, у яких необхідно установити, чи буде деяке твердження істинним у всіх математичних структурах визначеного типу. Наприклад, було показано, що проблема « є твердження, істинне для всіх груп» є нерозв'язною ( тут є твердження мовою числення предикатів першого порядку, що відповідає теорії груп), тоді як проблема « є твердження, істинне для всіх абелевих груп» розв'язна. (При цьому прийнято говорити, що теорія груп першого порядку нерозв'язна, у той час як теорія абелевых груп першого порядку розв'язна.) Як було показано Тарським [1951], проблема «твердження істинне в полі дійсних чисел» є розв'язної. З іншого боку, як ми побачимо в р. 8, багато проблем, зв'язаних з формалізацією арифметики натуральних чисел, нерозв'язні.

З іншими прикладами, а також з доведеннями багатьох результатів, що стосуються можливості розв'язання і нерозв'язності в математичній логіці, читач може ознайомитися в книгах Тарського, Мостовського і Робінсона [1953] чи Булоса і Джефрі [1974], а також Єршова [1981]*.

Размещено на Allbest.ru