Правило резолюцій — це правило висновування, що сходить до методу доказу теорем через пошук протиріч; використовується в логіці висловлювань і логіці предикатів першого порядку. Правило резолюцій, що застосовується послідовно для списку резольвент, дозволяє відповісти на питання, чи існує у вхідній множині логічих виразів протиріччя. Правило резолюцій запропоновано в 1930 році в докторській дисертації Жака Ербрана для доведення теорем у формальних системах першого порядку. Правило розроблено Джоном Аланом Робінсоном в 1965 році.

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

Логіка висловленьРедагувати

Правило резолюцій першочергово застосовується до диз'юнктів  — диз'юнкцій пропозиційних змінних чи їх заперечень. Правило застосовується до двох диз'юнктів у випадку, коли вони містять пропозиційні змінні, одна з яких є запереченням другої. Наприклад:

 

де   є доповненням  , (наприклад  , а  )

Для можливості використання цього правила необхідно записати формулу у кон'юнктивній нормальній формулі. Довільна формула логіки висловлень еквівалентна деякій формулі цього виду. При записі формули у кон'юнктивній формі кожен диз'юнкт можна подати як множину літералів (пропозиційних формул чи їх заперечень), а саму формулу як множину диз'юнктів. Наприклад формулу:

 

можна подати так:

 

Також таким чином можна визначити правило резолюцій:

  •  

Позначимо:

 , де   диз'юнкт одержаний за правилом резолюцій з деяких диз'юнктів формули   і: Mit   об'єднання всіх диз'юнктів одержаних з диз'юнктів формули   за скінченну кількість використань правила резолюцій.

Деяка формула   записана у КНФ є невиконуваною тоді і тільки тоді, коли  . Як наслідок з цього для довільних формул   формула   є логічним наслідком тих формул тоді і тільки тоді, коли  . Тобто система формального виводу заснована на правилі резолюцій є коректною і повною.

ПрикладРедагувати

Нехай є формули:

 
 
 

Потрібно довести що:

 

Спершу приведімо дані формули до кон'юнктивної нормальної форми:

 
 
 

Далі запишемо:

 

Послідовно використовуючи правило резолюцій отримуємо:

 
 
 

що й доводить твердження.

Числення висловлюваньРедагувати

Нехай   і   — дві пропозиції в численні висловлювань, і нехай  , а  , де   — пропозіціональная змінна, а   й   — будь-які пропозиції (зокрема, може бути, порожні або складаються тільки з одного літерала).

Правило виводу

 

називається правилом резолюцій.[1]

Пропозиції C1 і C2 називаються резольвуючими (або батьківськими), пропозиція    — резольвентою, а формули   і   — контрарними літералами. Загалом в правилі резолюції беруться два вирази і виробляється новий вираз, що містить всі літерали двох початкових виразів, за винятком двох взаємно обернених літералів.

Метод резолюціїРедагувати

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

Рішення в логічній моделі на основі методу резолюцій Дано твердження: «Сократ — людина»;

«Людина — це жива істота»;

«Всі живі істоти смертні».

Потрібно методом резолюцій довести твердження «Сократ смертний».

Рішення: Крок 1. Перетворимо висловлювання на диз'юнктивну форму;

Крок 2. Запишемо заперечення цільового виразу (необхідного виводу), тобто «Сократ безсмертний»;

Крок 3. Скласти кон'юнкцію всіх диз'юнктів, включивши в неї заперечення цільового виразу;

Крок 4. У циклі проведемо операцію пошуку резольвентів над кожною парою диз'юнктів;

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

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

Для доказу того, що формула   є логічним наслідком множини формул  , метод резолюцій застосовується наступним чином. Спочатку складається множина формул  . Потім кожна з цих формул приводиться до КНФ (сполучення диз'юнктів) і в отриманих формулах закреслюються знаки кон'юнкції. Виходить безліч диз'юнктів  . І, нарешті, шукається висновок порожнього диз'юнктів з  . Якщо порожній диз'юнкт виводимо з  , то формула   є логічним наслідком формул  . Якщо з   не можна вивести #, то   не є логічним наслідком формул  . Такий метод доведення теорем називається методом резолюцій .
Розглянемо приклад докази методом резолюцій. Нехай у нас є наступні твердження:

«Яблуко червоне і ароматне.»
«Якщо яблуко червоне, то яблуко смачне.»

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

X1 — «Яблуко червоне»,
X2 — «Яблуко ароматне»,
X3 — «Яблуко смачне».

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

  — «Яблуко червоне і ароматне.»
  — «Якщо яблуко червоне, то яблуко смачне.»

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

Логіка першого порядкуРедагувати

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

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

 

Нехай тепер   — формула записана у нормальній формі Сколема. Незважаючи на квантори загальності цю формулу можна подати як об'єднання диз'юнктів.

Позначимо:

 , де   диз'юнкт одержаний за правилом резолюцій з деяких диз'юнктів формули   і

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

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

ПрикладРедагувати

Доведемо, що формула є логічно загальнозначимою:   Спершу слід використати процедуру сколемізації:

 
 
 
 

Відкидаючи квантор загальності:

 
 

Далі послідовно використовується правило резолюцій:

 

заміна (x → a)

 

заміна (x → a)

що й доводить твердження.

Обчислення предикатівРедагувати

Нехай C1 та C2 — дві пропозиції в численні предикатів.

Правило виводу

 

називається правилом резолюції в численні предикатів, якщо в пропозиціях C1 та C2 існують уніфіцировані контрарні літерали P1 та P2, тобто  , а  , причому атомарні формули P1 и P2 є уніфікуючим найбільш загальним уніфікатором  ..

У цьому випадку резольвенти пропозицій C1 та C2 є пропозиція C1 и C2, отримане з пропозиції  застосуванням уніфікатора  .[2]

Однак внаслідок нерозв'зності логіки предикатів першого порядку для здійсненної (несуперечливої) множини диз'юнктів процедура, заснована на принципі резолюції, може працювати нескінченно довго. Зазвичай резолюція застосовується в логічному програмуванні в сукупності з прямим або зворотнім методом міркування. Прямий метод (від посилок) з посилок А, В виводить висновок В (правило modus ponens). Основний недолік прямого методу міркування полягає в його ненаправленості: повторні застосування методу зазвичай призводять до різкого зростання проміжних висновків, не пов'язаних з цільовим ув'язненням.
Зворотний метод (від мети) є спрямованим: з бажаного висновку В тих самих посилок він виводить новий подціловий висновок А. Кожен крок висновування в цьому випадку завжди пов'язаний з спочатку поставленою метою.

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

Висновок в логічних моделяхРедагувати

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

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

ПриміткиРедагувати

  1. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем стр. 77
  2. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем стр. 85

Див. такожРедагувати

ДжерелаРедагувати

  1. J. Alan Robinson (1965), A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM (JACM), Volume 12, Issue 1, pp. 23-41.
  2. Leitsch, Alexander (1997). The Resolution Calculus. Springer-Verlag.
  3. Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers.