Метод резолюций для логики предикатов

Основой метода резолюций для логики предикатов является крупноблочное правило, соединяющего в себе обобщенную подстановку и шаг логического вывода. Это правило и было названо правилом резолюции.

Дадим критерий, когда две последовательности термов с одинаковым числом членов могут быть приведены к одинаковому виду подстановкой вместо свободных переменных.

Определение.Подстановка—множество пар вида (x\ t), где x—переменная, t — терм, причем все первые члены в этих парах различны. Применение подстановки σ к терму t обозначается tσ и определятся индуктивно

1. xσ = t, если (x\ t) є σ.

2. xσ = x, если нет пары (x\ t) є σ.

3. cσ = c, c—константа.

4. f(t1, . . . , tn)σ = f(t1σ, . . . , tnσ).

Композиция подстановок σ и θ определяется следующим образом:

σ θ = {(x\ t θ) | (x\ t) є σ}.

Говорят, что σ накрывает (является более общей, чем) ϑ , пишется σ ≥ ϑ , если $ θ (ϑ = σ θ).

Если каждая из двух подстановок накрывается другой, то они эквивалентны.

Подстановка σ унифицирует последовательности термов t1, . . . , tn и r1, . . . , rn, если для всех i tiσ = riσ.

Теорема (об унификации).Для каждых двух унифицируемых последовательностей термов существует унифицирующая подстановка, накрывающая любую другую такую подстановку (являющаяся наиболее общим унификатором).

Доказательство. Проведем построение, которое за конечное число шагов даст такую подстановку σ либо выяснит, что ее нет.

Шаг 0. Вначале положим подстановку пустым множеством.

Шаг 1. Ищем в последовательностях пару термов, каждый из которых начинается с функционального символа. Если соответствующие функциональные символы различны, то две последовательности неунифицируемы, если же они совпадают, заменяем члены f(s1, . . . , sk) и f(q1,. . . , qk) на последовательности s1, . . . , sk и q1, . . . , qk, соответственно.

После этого шага во всех парах соответствующих друг другу термов хотя бы один член является переменной либо константой.

Шаг 2. Удаляем из последовательностей все одинаковые члены, находящиеся на одинаковых местах. Если после этого хотя бы в одном месте встретятся две соответствующие друг другу (различные) константы, унификация невозможна.

Теперь в каждой из пар термов хотя бы один является переменной.

Шаг 3. Если первой парой является пара (x\t), то если t содержит x, заключаем, что унификация невозможна, а если t не содержит x, то добавляем к σ пару (x\t), выбрасываем первые члены из двух последовательностей и заменяем остальные термы r на r{(x\t)}.

Если после этого появились пары, оба компонента которых не являются переменными, то возвращаемся к шагу 1.

Симметрично действуем в случае, когда переменной является второй компонент пары.

Шаг 4. Если длина обеих последовательностей дошла до 0, унифицирующая подстановка найдена.

Данный алгоритм всегда кончает работу, потому что в любом цикле количество переменных уменьшается хотя бы на 1. То, что построенная унификация накрывает все остальные, легко показать индукцией по построению.

Унифицирующая подстановка, накрывающая все остальные, называется наиболее общим унификатором.

Пример 1.Списки аргументов атомарных формул {Q(a,x,f(x)), Q(u,у,z)} унифицируемы подстановкой {u\a, x\у,z\f(у)},

а списки аргументов формул из {R(x,f(x)), R(u,u)} неунифицируемы.

Правило резолюции состоит в том, что для двух дизъюнктов вида

P(t1, . . . , tn) ∨ Q и P(r1, . . . , rn) ∨ R

сначала ищется подстановка σ, унифицирующая t1, . . . , tn и r1, . . . , rn (списки термов). Если она находится, то в результате применения правила получается дизъюнкт (Q ∨ R)σ.

Еще одной красивой находкой в методе резолюций явилось представление дизъюнктов как множеств атомов.

Поскольку в методе резолюций рассуждают от противного, формула считается доказанной, если в результате последовательности резолюций получается ложь, представлением которой служит пустой дизъюнкт.

Пример 2.(Чень, Ли)

Некоторые пациенты любят докторов.

Ни один пациент не любит знахаря.

Значит, ни один доктор — не знахарь.

Решение (этих же авторов).

Переведем посылки и заключения на формальный язык:

F1. $x(P(x) & "y(D(y) É L(x, y))), (?)

F2. "x(P(x) É "y(Q(y) É L(x, y))),

G. "x(D(x) É Q(x)).

Поскольку проверяемое утверждение имеет вид F1 & F2 ÉG, после отрицания оно переходит в F1 & F2 & G. При приведении к предваренной форме ни один квантор $ не попадает после ", так что ни одной сколемовской функции не появляется. В итоге мы получаем следующие дизъюнкты:

(1) P(a)

(2) D(y) ∨ L(a, y)

из F1,

(3) P(x) ∨ Q(y) ∨ L(x, y) из F2,

(4) D(b)

(5) Q(b)

из G.

Методом резолюций получается следующий вывод пустого дизъюнкта:

(6) L(a, b) резольвента (4) и (2)

(7) Q(y) ∨ L(a, y) резольвента (3) и (1)

(8) L(a, b) резольвента (7) и (5)

(9) □ резольвента (6) и (8)

Конец решения.

Пример 3 (Доказательство теоремы). Применим метод резолюций в доказательстве одной простой теоремы из теории групп.

В качестве исходной возьмем следующую аксиоматику теории групп:

F₁: "x,y,z ((xy)z=x(yz)),

F₂: "x,y $z(zx=y),

F₃: "x,y $z(xz=y).

Предположим, что нам надо доказать теорему G: $x"y (yx=y), т.е. что в группе существует правая единица.

Наша задача – установить, что формула G есть логическое следствие формул F₁, F₂, F₃.

Прежде, чем решать эту задачу, перейдем к другой сигнатуре. Введем символ трехместного предиката P, который интерпретируется следующим образом: P(x,y,z) означает, что xy=z.

В новой сигнатуре формулы F₁, F₂, F₃ и G запишутся так:

F₁^/="x,y,z,u,v,w (P(x,y,u)&P(y,z,v)&P(x,v,w) ÉP(u,z,w)),

F₂^/="x,y $z P(z,x,y),

F₃^/="x,y $z P(x,z,y),

G^/=$x "y P(y,x,y).

Сформируем множество T={F₁,F₂,F₃, G}, каждую из формул этого множества приведем к сколемовской нормальной форме и удалим кванторы общности (конъюнкция в сколемовских нормальных формах не появится). Получим множество дизъюнктов D₁,D₂,D₃,D₄:

D₁= P(x,y,u) Ú P(y,z,v) Ú P(x,v,w) ÚP(u,z,w),

D₂= P(f(x,y),x,y),

D₃= P(x,g(x,y)y),

D₄= P(h(x),x,h(x)).

Построим вывод пустого дизъюнкта из множества дизъюнктов D₁,...,D₄. Пусть эти дизъюнкты–первые дизъюнкты вывода. Заменим переменные в дизъюнкте D₂, получим дизъюнкт D₂^/=P(f(x^/,y^/),x^/,y^/).

Литералы P(x,y,u) из D1и D₂^/ унифицируются подстановкой s₁={x\f(x^/,y^/),y\ x^/, u\y^/}. Применим правило резолюций к D₁ и D₂ (и указанным литералам), получим дизъюнкт

D₅= P(x^/,z,v) Ú P(f(x^/,y^/)v,w) Ú P(y^/,z,w).

Далее, литерал P(f(x^/,y^/),v,w) из D5 и D₂ унифицируются подстановкой s₂={x^/\x,y^/\y,v\x,w\y}.

Правило резолюций, примененное к D₅ и D₂, дает дизъюнкт

D₆= P(x,z,x) ÚP(y,z,y).

Резольвентой дизъюнктов D₃ и D₆ будет дизъюнкт

D₇=P(y,g(y^/,y^/),y).

Для получения этой резольвенты заменим переменные в D₃, получим D₃=P(x^/,g(x^/,y^/),y^/) и используем подстановку s₃={x\y^/,z\g(y^/,y^/)}.

Наконец, из дизъюнктов D₄ и D₇ с помощью подстановки s₄={y\h(g(y^/,y^/)), x\g(y^/,y^/)} получаем

D8= □ - пустой дизъюнкт.