Алгоритм метода резолюций для проверки невыполнимости множества дизъюнктов в логике высказываний

Резольвента – разрешающее уравнение, разрешающая функция, разрешающие операторы.

Правилом резолюций в логике предикатов называется правило из дизъюнктов P (t ₁, …, t_n) F и P (s ₁, …, s_n) G, выводим дизъюнкт (F) (G), где – наибольший общий унификатор множества { P (t ₁, …, t _n); P (s ₁, …, s_n)}.

Дизъюнкт (F) (G) называется бинарной резольвентой первых двух дизъюнктов, а литералы P (t ₁, …, t_n) и P (s ₁, …, s_n) – отрезаемыми литералами.

Пример: Из дизъюнктов Q (a, f (x)) R (x) и Q (u, z) P (z)

можно выделить дизъюнкт – бинарную резольвенту исходных дизъюнктов

R (x) P (f (x))

используя подстановку = { u = a; z = f (x)}.

Правилом склейки в логике предикатов называется правило из дизъюнкта ◊ P (t ₁, …, t_n) … ◊ P (s ₁, …, s_n) F выводим дизъюнкт = (◊ P (t ₁, …, t_n)) (F),

где - наиболее общий унификатор множества { P (t ₁, …, t_n), …, P (s ₁, …, s_n)},

◊ - знак отрицания или его отсутствие.

Дизъюнкт = (◊ P (t ₁, …, t_n)) (F) называется склейкой первого дизъюнкта.

Пример: Правило склейки, применённое к дизъюнкту:

P (x, y) P (y, x) P (a, a) Q (x, y, v)

даёт дизъюнкт P (a, a) Q (a, a, v)

P (x, y) P (y, x) P (a, a) Q (x, y, v)

= { x = a, y = a } – НОУ

(P (x, y)) = P (a, a);

(Q (x, y, v)) = Q (a, a, v).

Резольвентой дизъюнктов D ₁ и D ₂ называется одна из следующих бинарных резольвент:

- бинарная резольвента дизъюнктов D ₁ и D ₂;

- бинарная резольвента склейки D ₁ и дизъюнкта D ₂;

- бинарная резольвента дизъюнкта D ₁ и склейки D ₂;

- бинарная резольвента склейки D ₁ и склейки D ₂.

Определение вывода в логике предикатов

Пусть S – множество дизъюнктов. Выводом из множества дизъюнктов S называется последовательность дизъюнктов D ₁, D ₂, …, D _n, такая, что каждый дизъюнкт D _i принадлежит S, выводим из предыдущих дизъюнктов по правилу резолюций или выводим из предыдущего по правилу склейки.

Пример: S = { B(x) C(x) T(f(x)), C(y) T(f(z)), B(a)}

Вывод из S – последовательность дизъюнктов:

D ₁ = B(x) C(x) T(f(x)) - S

D ₂ = C(y) T(f(z)) - S

D ₃ = B(x) T(f(x)) T(f(z)) – из D ₁ и D ₂ по правилу резолюций

D ₄ = B(x) T(f(x)) – из D ₃ по правилу склейки

D ₅ = B(a) S

D ₆ = T (f (a)) из D ₄ и D ₅ по правилу резолюций

Пример вывода по правилу резолюций

D ₁ = B(x) (C(x)) T(f(x)) - S

D ₂ = C(y) T(f(z)) - S

= {y = x}

D ₃ = B(x) T(f(x)) T(f(z)) – из D ₁ и D ₂ по правилу резолюций

 

Пример: по правилу склейки

D ₃ = B(x) T(f(x)) T(f(z))

= {z = x}

D ₄ = B(x) T(f(x)) из D ₃ по правилу склейки

Теорема о полноте: Множество дизъюнктов S логики первого порядка невыполнимо тогда и только тогда, когда из S выводим пустой дизъюнкт ().

Имеется множество гипотез (формул) {F₁, …, F_k}. Доказать, что формула G – логическое заключения множества гипотез. {F₁, …, F_k} G

Для доказательства этого также применяется метод резолюций.