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

Описываемый ниже алгоритм предназначен для ответа на вопрос: “Как применить теорему к выражению?” Этот алгоритм не зависит от формальной системы, в которой применяется. Для заданных теоремы и выражения алгоритм выполняет в строгой последовательности двойной проход в предварительно

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

Данный алгоритм, разработанный в 1966 г. Ж. Питра и независимо от него Дж. Робинсоном, играет фундаментальную роль в искусственном интеллекте.

3.7.1. Задача

Для данной теоремы Т в форме правила переписывания или продукции с антецедентом вида

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

Примеры унификации

1. Пусть алгебраическое тождество

рассматривается в качестве удобного сокращенного представления правила переписывания: “Если какое-то выражение является квадратом суммы двух термов, его можно переписать в виде суммы квадрата первого терма, удвоенного произведения обоих термов и квадрата второго терма”.

Пусть, кроме того, имеется выражение

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

2. Аналогично известное правило переписывания

применяется к выражению

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

Унификация также невозможна при использовании выражения

так как в этом случае требуется коммутативность относительно знака Это затруднение можно устранить с помощью использования правила

предварительное применение которого к выражению позволяет затем выполнить унификацию выражений

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

и пусть имеется метатеорема

Ниже показаны те возможные “естественные” подстановки, которые, однако, не являются оптимальными. Они приведут к правильному результату — частному выражению, которое, однако, не представляет большого интереса. Вспомним “правила игры”: в исчислении высказываний пропозициональные буквы и формулы являются свободными переменными. Все появления какой-либо переменной могут быть замещены термом, не содержащим замещаемой переменной. Чтобы привести к совпадению выражения и можно вначале сделать пробные шаги. Так, подстановка, преобразующая в в выражении дает

Изменим на так, чтобы унифицировать начальные символы выражений

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

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

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

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