8. Метод резолюций в исчислении предикатов

Зафиксируем некоторую сигнатуру Σ.

Подстановкой сигнатуры Σ называется конечное множество вида {t₁/x₁,...,t_n/x_n}, где t_i — терм сигнатуры Σ, отличный от переменных x_i (i=1..n), и все переменные х₁,...,х_п различны. Подстановка, которая не содержит элементов, называется пустой и обозначается через ε.

Мы будем использовать греческие буквы для записи подстановок.

Пример1. Множества {F₁(z)/x, y/z}, {c₁/x, F₂(y)/y, F₁(F₂(c₂))/z} — подстановки сигнатуры Σ = {F₁⁽¹⁾, F₂⁽¹⁾, c₁⁽⁰⁾, c₂⁽⁰⁾}.

Пусть θ = { t₁/x₁,...,t_n/x_n } — подстановка сигнатуры Σ, W — множество формул (термов) сигнатуры Σ. Тогда W θ - множество формул (термов) сигнатуры Σ, полученных из формул (термов) множества W заменой в них одновременно всех вхождений x_i (i=1..n) на термы t_i (i=1..n). При этом предполагается, что выполняются все условия на записи формул , W.

Если W = {Ф} или W = {t}, где Φ — формула, t — терм сигнатуры Σ, то вместо {Ф} и {t} будем писать Φ и t соответственно.

Пример 2. Пусть θ = { c₁/x, F₂(с₂)/y,y/z} — подстановка сигнатуры Σ = { c₁⁽⁰⁾, c₂⁽⁰⁾, . F⁽¹⁾, F₁⁽³⁾, }, t = F₁{x,y,z), Φ = (F(x)  F₁(x,c₁,z)). Тогда tθ=F₁(c_l,F(c₂),y), Φ = (F(c₁)  F₁(c₁,c₁, y)).

Пусть θ = { t₁/x₁,...,t_n/x_n } и λ = { q₁/y₁,...,q_m/y_m } — подстановки сигнатуры Σ. Тогда композиция подстановок θ и  (θ  ) есть подстановка, которая получается из множества { t₁/x₁,...,t_n/x_n, q₁/y₁,...,q_m/y_m } вычеркиванием всех элементов t_j/x_j, для которых t_j = x_j, и всех элементов q_i/y_i, таких, что y_i{x₁,..., х_п}.

Пример3. Пусть θ = { t₁/x₁, t₂/x₂} = {F(y)/x, z/y}, λ = {q₁/y₁, q₂/y₂, q₃/y₃} = {c₁/x,c₂/y,y/z} — подстановки сигнатуры Σ = { c₁⁽⁰⁾, c₂⁽⁰⁾, . F⁽¹⁾}. Тогда t₁/x₁, t₂/x₂, q₁/y₁, q₂/y₂, q₃/y₃} = {F(c₂)/x,y/y,c₁/x,c₂/y,y/z}. Так как t₂λ = у, то у/у должно быть вычеркнуто. Так как х, у  {х, у}, то c₁/x,c₂/y также должны быть вычеркнуты. Таким образом, θ о  = {F(c₂)/x, y/z}.

Подстановка θ сигнатуры Σ называется унификатором для множества {Φ₁,..., Φ_k} формул сигнатуры Σ, если Φ₁ = ... = Φ_k. Множество формул {Φ₁,..., Φ_k } сигнатуры Σ называется унифицируемым, если для него существует унификатор сигнатуры Σ.

Пример 4. Множество {P(c₁,y),P(x,F(c₂))} формул сигнатуры Σ = { c₁⁽⁰⁾, c₂⁽⁰⁾, P⁽²,⁾. F⁽¹⁾} унифицируемо, так как подстановка θ = {c₁/x,F(c₂)/y} является его унификатором.

Унификатор σ для множества { Φ₁,..., Φ_k } формул сигнатуры Σ называется наиболее общим унификатором (НОУ), если для каждого унификатора θ сигнатуры Σ этого множества существует подстановка  сигнатуры Σ такая, что θ = σ ο λ.

Пусть W = {Φ₁,..., Φ_k} — непустое множество атомарных формул сигнатуры Σ. Множеством рассогласований в W называется множество термов {t₁,...,t_k }, где t_i входит в Ф_i· и начинается с символа (который есть либо сигнатурный символ, либо переменная), стоящего на первой слева позиции в Ф_i·, на которой не для всех формул Φ₁,..., Φ_k находится один и тот же символ.

Пример 5. Пусть W = {P(x,F(y,z)),P(x,c), P(x, F(y,F₁(z))) — множество формул сигнатуры Σ = {Р⁽²⁾, F⁽²⁾, F₁ ⁽¹⁾}. Во всех трех формулах первые четыре символа Р(х, совпадают, а на пятом месте в первой и второй формулах стоят разные символы: F, с. Таким образом, множество рассогласований в W – { F(y,z),c, F(y,F₁(z))}.

Алгоритм унификации предназначен для распознавания того, является ли данное конечное непустое множество атомарных формул унифицируемым, и нахождения НОУ для этого множества в случае его унифицируемости.

Пусть W — конечное непустое множество атомарных формул. Алгоритм унификации для множества W:

Шаг 1. Полагаем k = 0, W_k = W,_k = ε.

Шаг 2. Если W_k — одноэлементное множество, то остановка: _k - НОУ для W. В противном случае найдем множество D_k рассогласований для W_k.

Шаг 3. Если существуют x_k,, t_k  D_k такие, что x_k — переменная, не входящая в терм t_k, то перейти к шагу 4. В противном случае остановка: множество W не унифицируемо.

Шаг 4. Полагаем _k+1=_k  { t_k / x_k } и W_k+1 = W_k{ t_k /x_k) (заметим, что W_k+1 = W_k+1)·

Шаг 5. Присвоить k значение k+1 и перейти к шагу 2.

Теорема 1. Если W — конечное непустое унифицируемое множество атомарных формул, то алгоритм унификации будет всегда заканчивать работу на шаге 2 и последняя подстановка σ_k будет НОУ для W.

Пример 6. Найти НОУ для множества W={Р(с,х,F₂(F₁(y))),P(z,F₂(z),F₂(u))}.

1. Положим k = 0, W₀ = W, σ₀ = ε.

2. Так как W — неодноэлементное множество, то σ₀ не является НОУ для W. Множество рассогласований для W₀ есть D₀ = {c,z}.

3. В D₀ существует переменная x₀ =z, которая не встречается в терме t₀ =c. Поэтому переходим к шагу 4.

4. Полагаем σ₁ = σ₀ {с/z} = ε  {с/z} = {с/z}, W₁=W₀(c/z) = { Р(с,х,F₂(F₁(y))),P(c,F₂(c),F₂(u))}.

5. Присваиваем k = 1.

6. Так как W₁— неодноэлементное множество, множество рассогласований для W₁ есть D₁ = {x,F₂(c)}.

7. Из D₁ находим, что х₁ = х, t₁ = F₂(c).

8. Полагаем σ₂ = σ₁ {F₂(c)/x}, W₂ = W₁{F₂(c)/x} ={Р(с, F₂(c), F₂(F₁(y))), P(c, F₂(c), F₂(u))}.

9. Присваиваем k = 2.

10. Так как W₂ — неодноэлементное множество, множество рассогласований для W₂ есть D₂ = {F₁(y),u}.

10. Из D₂ найдем, что х₂ = и, t₂ = F₁(y).

10. Полагаем σ₃ = σ₂ {F₁(y)/u} = {c/z,F₂(c)/x,F₁(y)/u}, W₃ = W₂{F₁(y)/u}={P(c, F₂(c), F₂(F!(y))), P(c, F₂(c),F₂(F₁(y)))} = {P(c,F₂(c),F₂(F₁(y)))}.

11. Множество W₃ одноэлементно. Поэтому σ₃ = {c/z,F₂(c)/x, F₁(y)/u} - НОУ для W.

Литерой сигнатуры Σ называется атомарная формула или отрицание атомарной формулы сигнатуры Σ. Дизъюнктом сигнатуры Σ называется литера сигнатуры Σ или дизъюнкция литер сигнатуры Σ.

Пусть Φ — дизъюнкт сигнатуры Σ вида ₁·…_n или ₁·…_n, где _i — атомарные формулы сигнатуры Σ (1 <= i <= n). Предположим, что множество формул {_{1, …},_п} имеет НОУ σ. Тогда ₁σχσ или соответственно ₁σχσ называется склейкой Ф. Полученную формулу в дальнейшем будем обозначать через Φσ.

Пример 7. В формуле Φ = Ρ (x)  P(F(y)) Р₂(x) подформулы Ρ(x) и P(F(y)) имеют НОУ σ = {F(y)/x}. Следовательно, Φσ = P(F(y))P₂(F(y)) — склейка Ф.

Пусть Φ₁, Ф₂ — два дизъюнкта, не имеющих общих переменных, L₁, L₂ — литеры в Φ₁ и Ф₂ соответственно. Если литеры L₁ и L₂^ L₂ имеют НОУ σ, то дизъюнкт, получаемый из дизъюнкта Φ₁σΦ₂σ вычеркиванием L₁σ и L₂σ, называется бинарной резольвентой Φ₁ и Ф₂, а литеры L₁ и L₂ называются отрезаемыми литерами. Если Φ₁σ = L₁ и Φ₂σ = L₂, то полагаем бинарную резольвенту Φ₁ и Ф₂ равной 0.

Если Φ₁ и Ф₂ имеют общие переменные, то, заменив в формуле Ф₂ эти общие переменные на переменные, не встречающиеся в Φ₁ и Ф₂, получим формулу Ф₂^, которая не имеет общих переменных с формулой Φ₁. Бинарной резольвентой формул Φ₁ и Ф₂ называется бинарная резольвента формул Ф₁ и Ф'₂.

Резольвентой дизъюнктов Φ₁ и Ф₂ (res(Φ₁,Φ₂)) является одна из следующих бинарных резольвент:

• бинарная резольвента Φ₁ и Ф₂;

• бинарная резольвента склейки Φ₁ и Ф₂;

• бинарная резольвента Φ₁ и склейки Ф₂;

• бинарная резольвента склейки Φ₁ и склейки Ф₂.

Пример 8. Найти res(Ф₁,Ф₂), где ;

Склейка , тогда

Пусть S — множество дизъюнктов сигнатуры Σ. Резолютивный вывод формулы Φ из S есть такая конечная последовательность Φ₁, ..., Ф_k дизъюнктов, что Φ_k: = Φ и каждый дизъюнкт Φ_i или принадлежит S, или является резольвентой дизъюнктов, предшествующих Ф_i.

Универсальным замыканием формулы Φ(x₁,... ,х_п) называется предложение  x₁,... ,х_п Φ(x₁,... ,х_п).

Теорема 2. (теорема о полноте метода резолюций). Если S — множество дизъюнктов сигнатуры Σ, то множество универсальных замыканий формул из S невыполнимо тогда и только тогда, когда существует резолютивный вывод нуля из S.

Пример 9. Доказать невыполнимость множества формул W = {Φ₁,...,Φ₆}, где

Φ₁=P₁(c₁,F(c₂),F(c₃)),

Φ₂= P₂(c₁),

Φ₃ = Ρ₁(x,x,F(x)),

Φ₄ = Ρ₁(x,y,z) Ρ₃(x,z),

Φ₅= Ρ₂(x) Ρ₁(y,z,u) Ρ₃(x,u)  Ρ₃(x,y)  Ρ₃(x,z),

Φ₆=Ρ₃(c₁, c₃).

Построим резолютивный вывод 0 из W:

Ф₇ = геs(Ф₂,Ф₅) = геs(Ф₂,Ф₅{z/y}) = Ρ₁(z,z,u) Ρ₃(c₁,u)  Ρ₃(c₁,z);

Ф₈ = res(Φ₃, Ф₇) = Ρ₃(c₁,F(x))  Ρ₃(c₁,x);

Ф₉ =res(Ф₆,Ф₈) =Ρ₃(c₁,F(c₃));

Ф₁₀ = геs(Ф₄,Ф₉) = Ρ₁(c₁,y, F(c₃))

Φ₁₁ =res(Φ₁,Φ₁₀) =0.

Пример 10. Показать выполнимо ли множество формул {Ф₁,Ф₂}?

;

Приведем формулы к ПКНФ:

. .

Приведем к КлНФ: Введением скулемовской константы с и функции F, получаем, что выполнимость формул Ф₁,Ф₂ сигнатуры равносильна выполнимости формул { , } сигнатуры или { }.

{ }.

, тогда множество формул – невыполнимо.

Следующий пример показывает, как формализуются предложения и методом резолюций эффективно доказываются теоремы при переходе к соответствующим формализациям.

Пример 11. Установить, что из посылки "Студенты суть граждане" следует заключение "Голоса студентов суть голоса граждан".

Пусть формулы S(x),C(x) и V(x,y) означают "х — студент", "х — гражданин" и "х есть голос у" соответственно. Тогда посылка и заключение запишутся следующим образом:

y(S(y)C(y)) (посылка),

x(y(S(y)V(x, у))  z(C(z) V(x, z))) (заключение).

Формула, соответствующая посылке, эквивалентна дизъюнкту - S(y)C(y). Так как

x(y(S(y)V(x, у))  z(C(z) V(x, z))) x(y(S(y)V(x, у))  z(C(z) V(x, z))) xyz(S(y)V(x, у)  (C(z) V(x, z)))  xyz(S(y)  V(x, у)  (C(z)  V(х, z))), имеем три дизъюнкта, определяющие отрицание заключения (а,в – скулемовские константы):

S(b), V(a,b),C(z)V(a,z).

Доказательство заканчивается следующим образом:

res(S(y)C(y), S(b))=C(b),

res(C(b), C(z)V(a,z))=V(a,b),

res(V(a,b),V(a,b))=0.

Т.о. теорема доказана.