12.1.2. Применение резолюции в общем случае

Для формирования резольвенты надо найти два предложения с дополняющими друг друга литералами. Это легко сделать для основного случая, поскольку дополнения нетрудно обнаружить. В общем случае дополняющие друг друга литералы можно найти подстановкой. Проиллюстрируем это другим примером из области неравенств. Пусть — переменные, принимающие целые положительные значения. Обозначим для ясности отношение «равно» через Е, а отношение „больше чем“ через G. Наконец, пусть произведение

обозначается Множество таких предложений и их интерпретации приведены в табл. 12.4.

Таблица 12.4

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

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

Сначала надо найти подходящую подстановку. При этом надо быть осторожным и не перепутать имена переменных из разных предложений. Поэтому переменные в левом предложении мы обозначим а в правом Тогда (30) примет вид

Правило подстановки заключается в том, что терм можно подставить вместо переменной, не содержащейся в нем, при условии, что эта подстановка непротиворечива. Новое высказывание есть специальный частный случай исходного предложения, называемый подстановочным частным случаем. Подставляя вместо в (31), получаем

Подстановка вместо дает

Для (33) можно провести резолюцию:

Затем можно разрешить Для этого опять во избежание путаницы переименуем переменные:

Подставляя вместо и 1 вместо проводим резолюцию и получаем

Итак, мы вывели и тем самым доказали, что исходное множество предложений невыполнимо.

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

Пусть А — множество атомов. Подстановкой 0 называют операцию

где соответственно терм и переменная из А. Когда применяется , каждый терм заменяет соответствующую переменную во всем множестве А. Новое множество атомов обозначается Будем также обозначать соответственно предложение и высказывание, получающиеся в результате замены всюду в С или в Пустая подстановка будет обозначаться через е.

Для любого множества атомов А можно построить множество рассогласования: сначала выделяется первая позиция, в которой не все атомы имеют одинаковые символы, а затем из всех атомов выписываются термы, начинающиеся с этой позиции. Например, если

то множеством рассогласования будет

Множество рассогласования пусто тогда и только тогда, когда все элементы А одинаковые.

Лексическое упорядочение — это такое упорядочение термов в множестве рассогласования, когда все переменные символы (если

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

Алгоритм унификации для множества атомов состоит из следующих шагов:

1. Положить и сделать подстановку пк=е.

2. Положить Если все элементы множества А одинаковы, то алгоритм заканчивает работу и сообщает об удаче, при этом (Отметим, что из определения подстановки следует, что последовательность подстановок есть также подстановка.) В противном случае продолжать работу.

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

4. Пусть первый и второй элементы лексически упорядоченного множества Если не является переменной или, будучи переменной, содержится в то алгоритм заканчивает работу и сообщает о неудаче. В противном случае положить и перейти к шагу 2.

Алгоритм унификации или сообщит о неудаче, если ни одна последовательность подстановок не сможет преобразовать все атомы множества А в одинаковые, или найдет нужную подстановку такую, что все элементы множества одинаковы. В этом случае будем говорить, что унифицирует А. Более того, — наиболее общий унификатор для А в следующем смысле. Предположим, что существует другая подстановка , которая также унифицирует А, но не порождается алгоритмом унификации. Унификатор всегда будет иметь вид

где — некоторая подстановка термов вместо переменных в Тогда подстановка унифицирует А и требует при этом наименьшего числа замен переменных константами и функциями. Однако не обязательно единственна.

Проиллюстрируем работу описанного алгоритма на примере. Пусть

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

(Необходимые переименования здесь уже выполнены.) Очевидные кандидаты для резолюции — литералы, содержащие так что

Применяя алгоритм унификации, получаем подстановку

Следовательно, резольвента для (41) имеет вид

Резолюция с унификацией представляет собой полный метод вывода (Робинсон, 1965). Сформулируем точное утверждение.

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

Этот важный результат гарантирует, что пустое предложение можно вывести из за конечное число шагов, если не является выполнимым. С другой стороны, неудача при выводе за какое-то конечное число шагов еще не означает, что выполнимо, поскольку пустое предложение быть может, удалось бы вывести за большее число шагов. Единственный способ доказать выполнимость множества — это достичь ситуации, когда нельзя сделать новых резолюций, при условии, что резолюции выбираются так, что свойство полноты сохраняется. Бывают случаи, когда это не происходит.