Алгоритм унификации для нахождения наиболее общего унификатора.

Пусть E – множество дизъюнктов, D – множество рассогласований, k – номер итерации, s_k наиболее общий унификатор на k-ой итерации.

Шаг 1. Присвоим k=0, s_k=e (пустой унификатор), E_k=E.

Шаг 2. Если для E_k не существует множества рассогласований D_k, то остановка: s_k – наиболее общий унификатор для E. Иначе найдем множество рассогласований D_k.

Шаг 3. Если существуют такие элементы v_k и t_k в D_k, что v_k переменная, не входящая в терм t_k, то перейдем к шагу 4. В противном случае остановка: E не унифицируемо.

Шаг 4. Пусть s_k+1=s_k { t_k / v_k}, заменим во всех дизъюнктах E_k t_k на v_k.

Шаг5. K=k+1. Перейти к шагу 2.

Пример 16. Рассмотрим дизъюнкты:

E={P(f(a), g(x)), P(y, y)}.

1. E₀=E, k=0, s₀=e.

2. D₀={f(a),y}, v₀=y, t₀=f(a).

3. s₁=={f(a)/y}, E₁={P(f(a), g(x)), P(f(a), f(a))}.

4. D₁={g(x),f(a)}.

5. Нет переменной в множестве рассогласований D₁.

Следовательно, алгоритм унификации завершается, множество E – не унифицируемо.

С помощью унификации можно распространить правило резолюций на исчисление предикатов. При унификации возникает одна трудность: если один их термов есть переменная x, а другой терм содержит x, но не сводится к x, унификация невозможна. Проблема решается путем переименования переменных таким образом, чтобы унифицируемые дизъюнкты не содержали одинаковых переменных.

Определение 34: Если два или более литерала (с одиниковым знаком) дизъюнкта C имеют наиболее общий унификатор s, то Cs - называется склейкой C.

Пример 16. Рассмотрим дизъюнкты:

Пусть C= P(x)Ú P(f(y))Ú ØQ(x).

Тогда 1 и 2 литералы имеют наиболее общий унификатор s = {f(y)/x}. Следовательно, Cs=P(f(y))Ú ØQ(f(y)) есть склейка C.

Определение 35: Пусть C₁ и C₂ – два дизъюнкта, которые не имеют никаких общих переменных. Пусть L₁ и L₂ - два литерала в C₁ и C₂ соответственно. Если L₁ и ØL₂ имеют наиболее общий унификатор s, то дизъюнкт (C₁s - L₁s) È (C₂s - L₂s) называется резольвентой C₁ и C₂.

Пример 17:Пусть C₁= P(x)Ú Q(x) и C₂= ØP(a)Ú R(x). Так как x входит в C₁ и C₂, то мы заменим переменную в C₂ и пусть C₂= ØP(a)Ú R(y). Выбираем L₁= P(x) и L₂=ØP(a). L₁ и L₂ имеют наиболее общий унификатор s={a/x}. Следовательно, Q(a)Ú R(y) – резольвента C₁ и C₂.

Алгоритм метода резолюций.

Шаг 1. Если в S есть пустой дизъюнкт, то множество невыполнимо, иначе перейти к шагу 2.

Шаг 2. Найти в исходном множестве S такие дизъюнкты или склейки дизъюнктов C₁ и C₂, которые содержат унифицируемые литералы L₁ Î C₁ и L₂ Î C₂. Если таких дизъюнктов нет, то исходное множество выполнимо, иначе перейти к шагу 3.

Шаг 3. Вычислить резольвенту C₁ и C₂ и добавить ее в множество S. Перейти к шагу 1.

Язык логического программирования ПРОЛОГ.

Проиллюстрируем принцип логического программирования на простом примере: запишем известный метод вычисления наибольшего общего делителя двух натуральных чисел – алгоритм Евклида в виде Хорновских дизъюнктов. При этом примем новую форму записи фразы Хорна, например ØPÙØQÙØRÙS будем записывать как S: - P, Q, R. Тогда алгоритм Евклида можно записать в виде трех фраз Хорна:

1. NOD (x, x, x): -.

2. NOD (x, y, z): - B (x, y), NOD (f (x, y), y, z).

3. NOD (x, y, z): -B (y, x), NOD (x, f (y, x), z).

Предикат NOD – определяет наибольший общий делитель z для натуральных чисел x и y, предикат B – определяет отношение «больше», функция f – определяет операцию вычитания. Если мы заменим предикат B и функцию f обычными символами, то фразы примут вид:

1. NOD (x, x, x): -.

2. NOD (x, y, z): - x>y), NOD (x- y), y, z).

3. NOD (x, y, z): -y>x), NOD (x, y- x), z).

Для вычисления наибольшего общего делителя двух натуральных чисел, например 4 и 6, добавим к описанию алгоритма четвертый дизъюнкт:

4. ÿ: - NOD (4, 6, z).

Последний дизъюнкт – это цель, которую мы будем пытаться вывести из первых трех дизъюнктов.