Правило резолюцій

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до навігації Перейти до пошуку

Правило резолюцій — це правило висновування, що сходить до методу доказу теорем через пошук протиріч; використовується в логіці висловлювань і логіці предикатів першого порядку. Правило резолюцій, що застосовується послідовно для списку резольвент, дозволяє відповісти на питання, чи існує у вхідній множині логічих виразів протиріччя. Правило резолюцій запропоновано в 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.