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

Існують комп'ютерні програми, котрі розроблено для автоматизації міркувань, виконуваних за допомогою доведення логічних теорем. У багатьох із цих про­грам використано правило виведення, відоме як резолюція. Правило резолюції записують у вигляді ρ ν q, q ν r |- ρ ν r. На основі цього правила Дж. Робінсон (G. Robinson) 1965 р. запропонував метод резолюцій автоматичного доведення логічних теорем.

Нехай формулу f записано в КНФ

f = d₁ ^ d₂ ^... ^ d_m.

Тут кожна з формул d_i (i = 1, 2,..., m) — літерал або диз'юнкція літералів. Форму­лу d_i називають елементарною диз'юнкцією, диз'юнктом або клаузою. Кількість літералів у формулі d_i називають рангом елементарної диз'юнкції. Розглядають також елементарну диз'юнкцію з рангом 0, яку позначають □; така диз'юнкція не містить жодного літералу. За означенням елементарну диз'юнкцію з рангом 0 уважають такою, що дорівнює F.

За принципом прямої дедукції формулу g можна вивести з формул f₁, f₂,..., f_n тоді й лише тоді, коли f₁ ^ f₂ ^... ^ f_n ^ g — суперечність. Так буде, якщо одна з формул f₁, f₂,..., f_n хибна чи формула g істинна. Нехай формулу f = f₁ ^ f₂ ^...... ^ f_n ^ g записано в КНФ f = d₁ ^ d₂ ^... ^ d_m, де d₁, d₂,..., d_m — її елементарні диз'юнкції. Очевидно, що цю КНФ можна записати у вигляді множини її еле­ментарних диз'юнкцій S = {d₁, d₂,..., d_m}. Множину S називають невиконанною, якщо формула f невиконанна Припустимо, що елементарні диз'юнкції d₁ і d₂ такі, що d₁ містить літерал l₁, контрарний до літералу l₂ з d₂. Викреслимо літерал l₁ із d₁ та l₂ з d₂; побудуємо диз'юнкцію решти літералів цих елементарних диз'юнкцій. Отриману елемен­тарну диз'юнкцію називають резольвентою.