Алгоритм унификации

Принцип резолюции

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

Действительно, если мы имеем дизъюнкты типа:

,

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

В этом случае имеем:

;

.

Резольвентой этих двух дизъюнктов будет дизъюнкт

.

А если взять два дизъюнкта

,

,

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

Прежде чем переходить к рассмотрению вопроса об унификации, введем некоторые понятия.

Пусть задано множество дизъюнктов

.

В этом множестве дизъюнктов и - составляющие дизъюнкты.

А выражения ; ; - называются литералами.

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

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

;

;

- константный (фундаментальный) случай литерала или атом, так как нет переменных.

Подстановки, примененные в рассматриваемом примере, можно обозначать следующим образом:

, здесь подставляется вместо , а вместо ;

;

А теперь переходим собственно к алгоритму унификации.

Пусть имеем дизъюнкты типа:

= ; = .
К этим дизъюнктам резольвента может быть получена только после применения к подстановки вместо и подстановки вместо . Для этого необходимо:

1. Проверить, можно ли применить резолюцию к и

2. Найти подходящую подстановку, допускающую резолюцию.

Такую проверку и вычисление подстановки осуществляет алгоритм унификации.

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

Подстановкой называется конечное множество вида , где - терм, а - переменная, отличная от ().

Подстановка называется фундаментальной, если все () являются фундаментальными термами.

Пусть - подстановка, а - литерал (выражение). Тогда называется примером выражения , полученного заменой всех вхождений в переменной () на вхождение терма . называется фундаментальным примером выражения , если - фундаментальная подстановка.

Рассмотрим применение алгоритма унификации к заданным дизъюнктам и .

Шаг 1. Необходимо сравнивать соответствующие термы дизъюнктов слева направо, пока не встретятся первые термы с одинаковыми функциональными символами, которые различаются переменными или константами. Создается множество, состоящее из этих термов, называемое множеством рассогласования. Для и первым множеством рассогласования будет .

Шаг 2. Для каждой переменной множества рассогласования проверяем, встречается ли она в каком-нибудь другом терме этого же множества.

Шаг 3. Если на предыдущем шаге получен положительный ответ, то дизъюнкты не унифицируемы, и применение алгоритма оканчивается неудачей. Если ответ отрицательный, осуществляем подстановку вместо переменной из множества рассогласования терма из этого множества. Для и применяем подстановку ={x/g(c)}. В результате и принимают вид

= ; .

Шаг 4. Продолжаем двигаться направо, снова выполняя пункты 1-3. Новым множеством рассогласования будет . Применение подстановки дает

= ; .

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

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

Пусть - множество дизъюнктов. Множество - первые слева термы, стоящие на соответствующих местах в дизъюнктах , среди которых есть, по крайней мере, два различных} называется множеством рассогласования .

Так, например, для для множества

первыми слева различными термами в и являются и . Таким образом, первым множеством рассогласования будет . После применения подстановки возникает несоответствие между термами и . Следующее множество рассогласования . В конце концов, алгоритм заканчивает свою работу, выдавая в качестве ответа множество подстановок, позволяющих унифицировать и , и затем применить к ним правило резолюции для исчисления высказываний. Это Множество подстановок называется общим унификатором (ОУ) дизъюнктов.

Например, для = и = общим унификатором является множество .

Если дизъюнкты не могут быть унифицируемы, алгоритм останавливается на шаге 2

Унификатор называется наиболее общим унификатором (НОУ), если для любого другого унификатора существует подстановка такая, что .

Для множества термов или атомов наиболее общий унификатор определяется единственным способом.

Рассмотрим механизм нахождения НОУ на примере.

Пусть имеем исходное множество , где - константа. Унификатором для является подстановка

.

Если подстановку применить к множеству , получатся следующие основные примеры:

;

Если теперь положить и , то можно показать, что .

Подстановка унифицирует рассматриваемые атомы. Следовательно, является наиболее общим унификатором.

Алгоритм унификации в формальном описании выглядит так.

Пусть - множество атомарных формул.

Шаг 0. (тождественная подстановка).

Шаг k. Мы уже построили подстановки .

Шаг (рекурсия).

1) Если = = … = ,

алгоритм заканчивает работу, выдавая в качестве наиболее общего унификатора.

2). Если для некоторых , тогда

а) строим множество рассогласования

;

б) осуществляем проверку вхождений (ПВ) переменных, то есть, проверяем для каждой переменной , содержится ли она в каком–либо другом элементе .

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

унифицируемо. Если множество вообще не содержит переменных, ПВ также дает положительный ответ. Если содержит переменную и терм , и ПВ дает отрицательный ответ, полагаем , избавляясь таким образом от несоответствия между в термах и .

Шаг . Повторяем шаги , для .

Теорема 1. Если унифицируемо, то алгоритм останавливается, выдавая в качестве ответа наиболее общий унификатор:

.

Теорема 2. (Теорема Дж. А. Робинсона) Применение алгоритма унификации к множеству атомов дает следующий результат:

Если унифицируемо, то алгоритм останавливается, выдавая в качестве ответа НОУ множества ;

Если не унифицируемо, то алгоритм останавливается, объявляя, что унификатора не существует.

Воспользуемся теоремами 1 и 2 для определения унифицируемости.

Пример 1. (Множество унифицируемо)

Пусть дано множество формул:

.

Определить, унифицируемо ли множество . Если да, найти НОУ.

Шаг 0: Полагаем .

Шаг 1: .

.

ПВ негативна.

Полагаем .

Шаг 2: .

.

ПВ негативна.

Полагаем .

Шаг 3: .

.

ПВ негативна.

Полагаем .

Шаг 4:

Ø.

Вывод: унифицируемо и его НОУ имеет вид

НОУ= .

Пример 2. (Множество не унифицируемо).

Дано множество формул:

.

Определить, унифицируемо ли множество . Если да, найти НОУ.

Шаг 0: Полагаем .

Шаг 1: .

.

ПВ негативна.

Полагаем .

Шаг 2: .

.

ПВ позитивна, так как встречается в .

Вывод. Множество не унифицируемо.

Пример 3. Пусть дано множество формул:

.

Определить, унифицируемо ли множество . Если да, найти НОУ.

Шаг 0: Полагаем .

Шаг 1: .

.

ПВ негативна.

Полагаем .

Шаг 2: .

.

ПВ негативна.

Полагаем .

Шаг 3: .

.

ПВ негативна.

Полагаем .

Шаг 4:

. Ø.

Вывод: унифицируемо и его НОУ имеет вид

НОУ= .

Дата добавления: 2015-06-27