Оценки высоты термов в наиболее общем унификаторе

• Автор: Конев, Борис Юрьевич
• Шифр специальности: 01.01.06
• Научная степень: Кандидатская
• Год защиты: 1998
• Место защиты: Санкт-Петербург
• Количество страниц: 100 с. : ил.

Оглавление

Введение
1 Оценки высоты термов в наиболее общем унификаторе
1.1 Основные понятия
1.1.1 Термы и меры сложности
1.1.2 Подстановки и задача унификации
1.1.3 Процедуры унификации
1.2 Оценки относительно разности глубин
1.2.1 Нижняя оценка
1.2.2 Верхняя оценка
1.3 Оценки относительно количества неизвестных не типа сечения
1.3.1 Нижняя оценка
1.3.2 Верхняя оценка
1.4 Оценки относительно количества неизвестных с различными путями
1.4.1 Нижняя оценка
2 Верхняя оценка высоты термов в выводах с сечениями
2.1 Исчисления KGL и IGL
2.2 Верхняя оценка высоты термов в выводе с сечениями
в исчислении KGL и IGL
Литература

Введение
Задача и алгоритм унификации
Задача унификации возникает и изучается во многих областях информатики и математической логики таких, как, например, автоматическое доказательство теорем, логическое программирование, обработка естественных языков, теория сложности и теория вычислимости.
В наиболее общем виде задача унификации является задачей, формулируемой следующим образом. По двум описаниям X и У определить, можно ли найти объект Z, удовлетворяющий обоим описаниям? Эта задача обычно уточняется как задача определения по двум термам первого порядка, существует ли подстановка термов вместо переменных, которая превращает исходные термы в идентичные. Такая подстановка называется унификатором. Помимо задачи определения, существует ли такая подстановка, ставится задача поиска алгоритма унификации, строящего унификаторы для заданной пары термов. Унификатор а называется более общим, чем унификатор т, если т может быть представлен в виде композиции т = Л о а для некоторой подстановки А. Унификатор называется наиболее общим, если любой другой унификатор может быть представлен в виде его композиции с некоторой подстановкой.
Первое упоминание о концепции унифицирующего алгоритма, выдающего наиболее общий представитель множества всевозможных примеров, может быть найдено в дневниках и записках Э. Поста, относящихся к 20-м годам и опубликованных в 60-е годы в [17]. Явное описание алгоритма унификации впервые встречается в диссертации

Ж. Эрбрана [27], в которой он вводит три концепции допустимости формул. Он называет их А, В и С. Концепции В и С лежат в основе известной теоремы Эрбрана. Для проверки того, что формула удовлетворяет концепции А, Эрбран приводит вычисляющий её алгоритм. В этой работе употреблялась техника, переоткрытая позднее А. Мартелли и У. Монтанари [36], которая используется и по сей день.
Основываясь на идеях Эрбрана о конечном опровергающем примере, Д. Правиц [41] в 1960 году предложил алгоритм, основанный на последовательном переборе выводимых формул, позднее получивший название “Алгоритм Британского Музея”, в котором используется процедура, вычисляющая наиболее общий представитель множества всевозможных примеров. Однако, поскольку в его логике не содержалось функциональных знаков, реальных вычислений было не так уж много. В 1963 г. М. Девис [16] опубликовал процедуру вывода, объединяющую достоинства процедуры Правица и процедуры Девиса-Патнема [19, 18]. В реализации этой новой процедуры был использован алгоритм унификации, что явилось первым практическим воплощением данного алгоритма.
В 1965 г. в работе [42] Дж.А. Робинсон ввел формальное определение алгоритма унификации для термов первого порядка, вычисляющего наиболее общий унификатор. Именно в этой работе была установлена роль унификации как части процедуры автоматического вывода. Примерно в это же время, в 1965-69 гг., в Ленинградском отделении Математического института им. В.А. Стеклова велись работы по разработке алгоритмов автоматического вывода на основе обратного метода С.Ю. Маслова [2]. В реализации этого метода была использована процедура унификации, однако она не была отдель-

руемости других, используя свойства операций редукции термов и элиминации неизвестной, сформулированные на стр. 20, не ссылаясь явно на эти свойства при каждом применении указанных преобразований.
Доказательство леммы 1.2. Доказательство достаточно очевидно. Однако мы приводим его здесь для того, чтобы продемонстрировать технику, с помощью которой могут быть доказаны аналогичные простые утверждения, встечающиеся в дальнейшем.
Необходимость: пусть Апь) и Впб) унифицируемы. Тогда существует такая подстановка а, что
Отсюда следует, что <т(/(/(../(<) ...))) = сг(/(/(- fЫ ))) Тогда, оД) зг а(хп). Аналогично, а(хп) &(Д). Таким образом, оД)
Достаточность: пусть термы tut1 унифицируемы. Тогда существует наиболее общий унификатор а термов t и t'. Так как хп не входит в термы tut', а а — наиболее общий унификатор, значение подстановки о на неизвестной хп совпадает с хп. Рассмотрим подстановку
5 2" раз
5 2п раз
a(t), если х = хп,
а (х) = <