12.3.5. Пример из теории групп

Рассмотрим работу стратегии очищения с. п. л. на примере доказательства следующего факта из теории групп:

Теорема. В любой ассоциативной системе, в которой все уравнения вида имеют левое и правое решения и существует правый единичный элемент.

Доказательство. Применим стратегию с. п. л. и воспользуемся понятием несущего множества. Как и в стратегии упорядочения, здесь будут предпочитаться предложения с меньшим числом предикатов. Это включает в себя и предпочтение одночленов. Указанные стратегии определяют выбор предложения с которого начинается вывод, и последовательно на каждом шаге они ограничивают множество резолюций. Наш способ доказательства наглядный, но есть другие, более короткие и более изящные (см., например, Слейгл (1971)).

Первый шаг доказательства состоит в формализации рассматриваемой задачи. Пуать — предикат

Множество определим так:

Анализируя этот пример, мы должны будем так делать подстановки в предложениях х и у, чтобы не возникало неоднозначности в обозначениях. Будем обозначать переменные х, во всех левых родительских предложениях С через Эти же переменные во всех правых родительских предложениях В будут обозначаться

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

Сначала попытаемся унифицировать с одночленами это не удается. Затем в качестве возьмем переименовав переменные:

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

и разрешение приводят к

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

Теперь для упорядочения возможных резолюций с применяем стратегию предпочтения одночленов. После переименования переменных предложений принимает вид

что и определяет Унифицируя при помощи подстановки

получаем резольвенту

Меняя в ней индексы у переменных, окончательно находим

Но это не единственно возможная резольвента так как можно было бы получить другую резольвенту, разрешая и тем самым формируя другую ветвь линейного вывода, начинающуюся с Помня об этом, продолжаем прежний линейный вывод с (74). Последнюю альтернативу мы выбрали потому, что правило отбора предложений для участия в резолюции таково, что сначала пробуются предложения с меньшим числом литералов, а затем идет вывод с более длинными предложениями. Предложение можно разрешить с Си беря его 2-й литерал в качестве литерала резолюции. В результате подстановки

получаем

Заметим, что альтернативно 1-й литерал предложения можно было разрешить, используя Мы не будем рассматривать эту альтернативу, а просто на рис. 12.9 укажем возможность другого хода доказательства. Продолжая с (76), находим, что можно

разрешить с После смены индексов у переменных предложения и подстановки

получаем резольвенту

Теорема доказана. Последний шаг вывода соответствует нижней части левой ветви дерева, изображенного на рис. 12.9.

Рис. 12.9. Дерево с. п. л. - вывода пустого предложения для задачи (65).