Системи штучного інтелекту

Метод резолюцій як основа логічного виведення

Метод резолюцій – логічне числення у мові логіки предикатів першого порядку, що використовує єдине правило виведення (т.зв. правило резолюції). Для мови численні висловлювань це правило формулюється так: із формул AÚE та BÚØE, де E - елементарна формула, виводиться формула AÚB, а з EÚØE – виводиться "порожня" формула. Цього єдиного правила достатньо для встановлення того, чи є тотожно хибною довільна задана формула числення висловлювань, що подана в кон’юнктивній нормальній формі (КНФ). А саме, кон’юнкція скінченої множини М формул числення висловлювань, кожна з яких є диз’юнкцією елементарних формул і/чи їх заперечень, тотожно хибна тоді і тільки тоді, коли за допомогою правила резолюції із М виводиться порожня формула. Для логіки предикатів першого порядку правило резолюції формулюється більш складно - з використанням процедури уніфікації. Метод резолюцій вперше запропонував Дж.Робінсон в 1964. Його застосовують в мовах логічного програмування, при пошуку доведень теорем на ЕОМ, в доведеннях правильності програм, в системах планування поведінки роботів, в "питально-відповідальних" системах та ін. системах штучного інтелекту. Існують різні модифікації методу резолюцій, а також його узагальнень.

Системи штучного інтелекту