Метод резолюции в ЛППП.

Литеры L₁ и L₂ называются контрарными, если они являются отрицанием друг друга c точностью до унификации (то есть одна из литер изначально является отрицанием другой или ее можно таковой сделать с помощью подстановки).

Примечание. Формальное определение подстановки будет приведено ниже.

Бинарной резольвентой клозов С₁ и С₂, содержащих контрарные литеры L₁ и L₂ назовается клоз C, полученный следующим образом:

С={C₁\L₁}È{C₂\L₂}

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

Примеры.

//примеры - без подстановки и с подстановкой (6)

P (x) Ú Q (x, y) ù P(x) Ú R(z) Q(x, y) Ú R (z)

P (x) Ú Q (x, y) ù P(a) Ú R (z) {a/x} Q(a, y) R (z)

 

Доказано, что бинарная резольвента является логическим следствием.

В отличии от ЛВ, в ЛППП различают понятия резольвенты и бинарной резольвенты. Для того, чтобы определить понятие резольвенты необходимо рассмотреть подстановки.

Множество вида /подстановка (7)/ {t_i/x_i, … t_n/x_n}, где t_i – термы, а x_i – переменные называется подстановкой термов t_i вместо переменных x_i.

Если E – клоз, а Θ – подстановка, то EΘ – подстановочный частный случай, получаемый вследствие замены переменных x_i на термы t_i.

Пример.

//пример (8)

P (x) Ú Q (f (x), b, y)

{a/x, c/y}

P (a) Ú Q (f (a), b, c)

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

Пусть даны 2 подстановки Θ и Ω. Применим подстановку Θ, а затем подстановку Ω. Тогда будем говорить, что применили композицию подстановок ΩΘ.

Подстановка Θ называется унификатором множества выражений {E₁,..,E_n}, если E₁Θ =E₂Θ =….=E_nΘ.

Подстановка Ω - есть наиболее общий унификатор множества выражений {E₁,…,E_k}, если любой унификатор это множества выражений Θ можно получить путем композиции Ω с некоторой подстановкой Ψ. (Θ= ΩΨ).

П. С – дизъюнкт, а Θ - наиболее общий унификатор двух и более его литер, тогда СΘ называется склейкой дизъюнкта С.

Пример.

//пример склейки (9)

P (x) Ú Q (f(x), b, y) Ú P (a)

{a/x)

P (a) Ú Q (f(x), b, y)

Резольвентами дизъюнктов С₁ и С₂, содержащих контрарные литеры L₁ и L₂ называются бинарные резольвенты:

A) клозов С₁ и С₂;

B) любой склейки клоза C₁ и клоза С₂;

C) клоза С₁ и любой склейки клоза С₂;

D) любых склеек клоза С₁ и С₂

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

Примечание. Фактически, вывод сводится к последовательности вычисления бинарных резольвент и склеек.

Пример.

Аксиома 1. Мао Цзедун – человек

Аксиома 2. Все люди смертны.

Теорема. Мао Цзедун – смертен.

//пример формализации и вывода (10)

Вводим предикаты:

C (x) – x - человек

S (x) – x - смертен

Аксиома 1 C (Мао)

Аксиома 2 [C (x) → S (x)] =

Теорема S (Мао)

 

С (Мао) S (Мао)

ù С (x) Ú S (x) {Мао / x}

S (Мао) ù S (Мао)

Здесь также справедлива теорема о полноте резолютивного вывода. Множество клозов S противоречиво, если и только если существует резолютивный вывод пустого клоза из S.

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

Формальный алгоритм незначительно отличается от имеющегося в ЛВ.

ВХОД: S – входное множество клозов.

ВЫХОД: OK – удается получить пустой клоз, NO – не удается.

M:=S; // - M-текущее множество клозов.

while ÏM do

if not Choose (M, C₁, C₂, p₁, p₂) then return(NO);

N:=R(M, C₁, C₂, p₁, p₂); // - вычисление резольвенты.

M:=M È N; // - пополнение текущего множества.

end

return (OK); //получен пустой клоз

Примечание. Результат функции R здесь множество возможных резольвент клозов С₁ и С₂, содержащих контрарные литеры р₁ и р₂.