Автоматичний доказ теорем
У основі методу автоматичного (реалізованого програмно) докази теорем лежить апарат математичної логіки. Для простоти викладу ми наведемо необхідне математичне обґрунтування методу та розглянемо процес доказу на прикладі логіки висловлювань. Наприкінці ми обговоримо специфічні моменти, пов'язані з доказом теорем у логіці предикатів. Почнемо виклад з основних визначень та понять логіки висловлювань.
Вислів — це оповідальна пропозиція, про яку можна сказати істинно вона чи хибно. Наприклад, "Земля крутиться" - це справжнє висловлювання, а "Земля плоска" - хибне. Кажуть, що "істина" та "брехня" є значеннями істинності висловлювання. Позначатимемо такі прості (атомарні) висловлювання великими латинськими літерами, істину — одиницею, а брехня — банкрутом.
З простих висловлювань можна складати складні у вигляді застосування логічних операцій. Символи, що позначають логічні операції, називають зв'язками. Як приклад висловлювань, що містять логічні операції, можна навести такі. Нехай X та Y — деякі висловлювання. Тоді:
| Висловлювання | Назва логічної операції | Зв'язування |
| "X та Y" | кон'юнкція |
Істинність висловлювань, які у результаті цих операцій, визначається за такими правилами. Кон'юнкція висловлювань є істинною, якщо всі операнди істинні. Диз'юнкція істинна, якщо хоча б один операнд є істинним. Заперечення істинно, якщо операнд покладено. Про імплікацію X - & gt; Y (якщо X, то Y) кажуть, що X - посилкаімплікації, а Y - укладання імплікації. Імплікація хибна, якщо посилка імплікації істинна, а висновок хибно. Інакше імплікація істинна.
Залежність значення істинності складного висловлювання зазвичай зображують як таблиці істинності зв'язок. Для основних логічних операцій ця таблиця має такий вигляд.
Будь-яке складне висловлювання можна призвести до висловлювання, що містить лише логічні операції диз'юнкції, кон'юнкції та заперечення.
Формальна логіка висловлювань займається аналізом висловлювань, у своїй основну увагу приділяється формі висловлювання у відволіканні змісту. Формальним поданням висловлювання є формула. Формула визначає форму висловлювання, але не несе жодної інформації щодо суті висловлювання. Формули складаються з літер та зв'язок. Формула, яка не містить зв'язок, називається атомарною формулою. Атомарні формули позначатимемо літерами з кінця латинського алфавіту: U,V,W,X,Y та Z, позначені або непомічені нижнім індексом. До атомарних формул відносяться також 0 і 1. Неатомарні формули будемо позначати літерами F або G (також допустимо нижній індекс) або записувати в розгорнутій формі (через атомарні формули і зв'язки).
Надалі в інтерпретації нас цікавитимуть лише значення істинності висловлювань. Тобто. формули ми інтерпретуватимемо в "істину" або "брехню". Тоді те, що формула X інтерпретації j істинна, можна записати як j(X)=1.
Одна з основних цілей вивчення логіки полягає у отриманні формального апарату для доказу того, чи є це твердження наслідком інших.
Формула G називається логічним наслідком формул F1, F2. Fk якщо для будь-якої інтерпретації j з того, що j(F1)=j(F2)=. =j(Fk)=1 випливає, що j(G)=1.
Поняття логічногоНаслідки тісно пов'язані з поняттям здійсненності.
Безліч формул 1, F2. Fk> називається здійсненним, якщо існує інтерпретація j така, що j(F1)=j(F2)=. =j(Fk)=1.
Перевірку здійсненності множини формул 1,F2. Fk> можна провести побудовою спільної таблиці істинності цих формул. Якщо знайдеться хоча б один рядок, в якому в стовпцях формул F1, F2. Fk стоять одиниці, то це безліч формул можна здійснити. Якщо такого рядка немає, то безліч формул неможливо.
Теорема. Формула G є логічним наслідком формул F1, F2. Fk і тоді, коли безліч формул L=1,F2. Fk, ¬G> нездійсненно.
Доказ. Нехай формула G є наслідком множини формул F1. Fk. Припустимо, від неприємного, що безліч L можна здійснити. Це означає, що є інтерпретація j така, що j(F1)=. =j(Fk)=j(¬G)=1. Але якщо j(F1)=. =j(Fk)=1, то j(G)=1, оскільки G — логічний наслідок формул F1. Fk. Отримане протиріччя j(G)=1 і j(G)=1 доводить, що безліч формул 1. Fk, G> нездійсненно.
Нехай тепер безліч формул L нездійсненно. Розглянемо інтерпретацію j таку, що (F1) =. =j(Fk)=1. Оскільки L нездійсненно, то j(¬G)=0. Якщо j(G)=0, то j(G)=1. Отже, з рівностей (F1) =. =j(Fk)=1 слідує рівність j(G)=1. Це означає, що G — логічний наслідок множини формул F1. Fk.
Доказ теорем зводиться до того, що деяка формула G (гіпотеза теореми), є логічним наслідком безлічі формул F1. Fk (допущень). Тобто. сам текст теореми може бути сформульований так "якщо F1. Fk істинні, то істинна і G". Такий метод доказу теорем називається методом резолюцій.
Як було показано раніше, завдання про логічне слідство може бути зведене до завданняпро здійсненність. Формула G є логічним наслідком формул F1, F2. Fk і тоді, коли безліч формул 1,F2. Fk, G> нездійсненно. Метод резолюцій якраз і займається тим, що встановлює нездійсненність такої множини формул.
Перш, ніж ми опишемо сам метод, необхідно запровадити ще низку понять.
Літералом називається атомарна формула або її заперечення. Диз'юнктом називається диз'юнкція літералів. Диз'юнкт може складатися із одного літералу. Порожній диз'юнкт - це спеціальний диз'юнкт, що не містить літералів. Позначатимемо його #. Вважається, що порожній диз'юнкт складений за будь-якої інтерпретації. Порожній диз'юнкт, по суті, є атомарною формулою 0, але в контексті методу резолюцій прийнято користуватися #. Літерали X і X називаються протилежними.
Метод резолюцій ґрунтується на правилі резолюції.
Правило резолюції. З диз'юнктів (X v F) і (X v G) виводимо диз'юнкт (F v G). Або іншими словами, диз'юнкт (F v G) є логічним наслідком диз'юнктів (X v F) і (X v G).
Тобто. якщо j(X v F)=1 і j(X v G)=1 для деякої інтерпретації j, то j(F v G)=1. Це легко довести. Нехай j(X v F)=1 і j(X v G)=1. Тоді, якщо j(F)=1, то j(F v G) = 1. Якщо ж j(F)=0, то j(X) має дорівнювати 1, оскільки j(X v F)=1. Але тоді j(X)=0. Отже, j(G)=1, оскільки j(¬X v G)=1. Але якщо j(G)=1, то j(F v G) = 1.
Введемо поняття виводу. Нехай S - безліч диз'юнктів. Виводом із S називається послідовність диз'юнктів D1,D2. Dn така, що кожен диз'юнкт цієї послідовності належить S або випливає з попередніх правил резолюцій. Диз'юнкт D виводимо S, якщо існує висновок S, останнім диз'юнктом якого є D.
Застосування методу резолюцій ґрунтується на наступному твердженні, якеназивається теоремою про повноту методу резолюцій.
Теорема. Безліч диз'юнктів логіки висловлювань S нездійсненно тоді і лише тоді, коли з S виводимо порожній диз'юнкт.
Сам метод резолюцій можна сформулювати в такий спосіб.
Метод резолюцій. Для доказу, що формула G є логічним наслідком безлічі формул F1. Fk метод резолюцій застосовується в такий спосіб. Спочатку складається безліч формул 1. Fk, G>. Потім кожна з цих формул наводиться до нормальної кон'юнктивної форми (кон'юнкція диз'юнктів) і в отриманих формулах закреслюються знаки кон'юнкції. Виходить безліч диз'юнктів S. І, нарешті, шукається виведення порожнього диз'юнкту S. Якщо порожній диз'юнкт виводимо з S, то формула G є логічним наслідком формул F1. Fk. Якщо S не можна вивести #, то G не є логічним наслідком формул F1. Fk.
Розглянемо приклад докази шляхом резолюцій. Нехай ми маємо такі твердження:
- "Яблуко червоне та ароматне."
- "Якщо яблуко червоне, то яблуко смачне."
- X1 - "Яблуко червоне."
- X2 - "Яблуко ароматне."
- X3 - "Яблуко смачне."
- X1 & X2 - "Яблуко червоне та ароматне."
- X1 -> X3 - "Якщо червоне яблуко, то яблуко смачне."
Тепер наводимо всі формули до нормальної кон'юнктивної форми і закреслюємо кон'юнкції. Отримуємо таку безліч диз'юнктів:
Шукаємо виведення порожнього диз'юнкту (у цьомувисновку третій та останній елементи отримані за правилом резолюції, решта є елементами вихідної множини диз'юнктів):
Отримали порожній диз'юнкт, означає твердження про те, що яблуко смачне вірно.
Метод резолюцій можна застосувати і до логіки предикатів першого порядку (далі просто логіка першого порядку). Однак, щоб зробити метод робітником, потрібно внести низку змін та доповнень до версії для логіки висловлювань. Ми не вдаватимемося тут у подробиці. Зазначимо лише ті моменти, куди слід звернути увагу під час переходу від логіки висловлювань до логіки першого порядку.
У обчисленні першого порядку ми стикаємося з таким поняттям, як змінна. Тому правило резолюцій треба доповнити можливістю виконувати підстановку. Грубо кажучи, підстановкою називається безліч рівностей між змінними та термами. Підстановка називається уніфікатором деякої множини атомарних формул, якщо в результаті підстановки всі атомарні формули множини стануть однаковими. Якщо множина уніфікована, то існує, як правило, не один уніфікатор цієї множини, а кілька. Серед усіх уніфікаторів даної множини виділяють, так званий, найбільш загальний уніфікатор. Не визначатимемо тут це поняття. Тут нам важливо лише зрозуміти, що уніфікатор — це підстановка, яка робить елементи певної множини атомарних формул однаковими. Зазначимо, що існує метод отримання найбільш загального уніфікатора будь-якої безлічі атомарних формул.
У цій термінології правило резолюцій для логіки першого ладу можна записати так.
Правило резолюції. З диз'юнктів (P(t1. tn) v F) та (¬P(u1. un) v G) виводимо диз'юнкт (s(F) v s(G)), де s — найбільш загальний уніфікатор множини 1. tn), P (u1. un) & gt;.
Диз'юнкт, що вийшов(s(F) v s(G)) називають резольвентою.
На відміну від логіки висловлювань, у логіці предикатів нам знадобиться ще одне правило, яке називається правилом склеювання.
Правило склеювання. 1. З диз'юнктів (P(t1. tn) v P(u1. un) v F) виводимо диз'юнкт (s(P(t1. tn)) v s(F)), де s — найбільш загальний уніфікатор множини 1. tn), P (u1. un) & gt;. 2. З диз'юнктів (¬P(t1. tn) v ¬P(u1. un) v F) виводимо диз'юнкт (s(¬P(t1. tn)) v s(F)), де s — найбільш загальний уніфікатор множини 1. tn ), P(u1. un).
Диз'юнкт, що вийшов (s(P(t1. tn)) v s(F)) називають склейкою (те ж стосується і диз'юнкту з запереченням).
Визначення поняття виведення у логіці першого порядку трохи відрізняється від аналогічного визначення у логіці висловлювань. Висновок з безлічі диз'юнктів S називається послідовність диз'юнктів D1, D2. Dn така, що кожен диз'юнкт цієї послідовності належить S або виводимо з попередніх диз'юнктів за правилом резолюцій або за правилом склеювання.
В іншому метод резолюцій для логіки першого порядку нічим не відрізняється від методу для логіки висловлювань. Все зводиться до нездійсненності множини диз'юнктів. А безліч диз'юнктів S логіки першого порядку нездійсненно тоді і лише тоді, коли з S виводимо порожній диз'юнкт.