Способ представления термов в логике предикатов первого порядка

Размещено на http://www.allbest.ru/

Способ представления термов в логике предикатов первого порядка

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

В настоящее время в алгоритмах доказательства теорем, как правило, используются достаточно простые и экономные структуры представления термов, которые очень хорошо сочетаются и с процедурой дедуктивного вывода, и с процедурой унификации. Такими структурами часто являются ориентированные ациклические графы и плоские термы Касьянов и др., 2003 Christian, 1993. Достоинством ациклических орграфов является реализация всевозможных операций просмотра термов в разных направлениях и манипулирования их частями. Главным их недостатком является усложнение работы с памятью, из-за того, что размер каждого узла в первую очередь зависит от количества потомков. Однако этого нельзя сказать о плоском представлении термов. Достоинством плоских термов является предоставление удобного способа прямого разбора терма и значительное упрощение работы с памятью, из-за фиксированной структуры.

При разработке эффективного и простого в использовании представления термов необходимо объединение достоинств вышеописанных структур. Для этого необходимо решить две основные задачи: определение основной структуры представления термов и расширение такой структуры для удобного хранения в памяти. В качестве основной структуры представления термов предлагается использование размеченных ациклических орграфов , формальное определение которых описывается с помощью составного объекта , при условии , где - множество меток, - множество натуральных чисел, - множество вершин, - начальная вершина, - функция разметок вершин, - множество упорядоченных связей, таких, что , Касьянов и др., 2003 Капитонова и др., 2004 Андерсон, 2003 Дистель, 2002.

Для удобного описания термов рассматриваются только инициальные составные объекты, т.е. объекты для любой вершины которых, , где - транзитивное замыкание отношения непосредственной достижимости. Каждая вершина составного объекта S порождает составной объект, начальной вершиной которого является она сама. Причем i-м аргументом составного объекта , порожденного вершиной v, при условии существования такой, что , является составной объект , порожденный вершиной .

Задача представления терма размеченным ациклическим орграфом составного объекта S дополняется префиксным способом прохождения вершин с расстановкой на ребрах порядковых номеров потомков заданного родителя. Для этого выполняются следующие действия:

исследуется корневая вершина терма ;

рассматривается самый левый аргумент вершины , который еще ни разу не рассматривался ;

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

Пример 1. На рисунке 1 терм представлен размеченным ациклическим орграфом составного объекта S.

Размещено на http://www.allbest.ru/

Рис. 1. Представление терма в виде размеченного ациклического орграфа составного объекта S

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

Рассмотрим терм, имеющий вид:

,

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

Тогда символ * имеет путь на орграфе, который можно сформулировать в виде строки:

,

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

Этот путь имеет обозначение ПУТЬi(*), где i есть порядковый номер пути.

Пример 2. На рисунке 1 к переменной x1 имеется несколько путей:

ПУТЬ1(x1) := f1;

ПУТЬ2(x1) := f2g1;

ПУТЬ3(x1) := f4h1;

ПУТЬ4(x1) := f6k1.

Для расширенного представления термов также используются две дополнительные операции: ТИП(*) - тип висячей вершины орграфа (переменная, обозначаемая символом v и константа, обозначаемая символом c), КВАНТОР(*) - в области действия какого квантора находится переменная.

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

Пример 3. На рисунке 2 приведено расширенное задание терма в виде массива, взятого из примера 1.

Размещено на http://www.allbest.ru/

Рис. 2. Представление терма в виде массива

Для создания эффективных процедур дедуктивного вывода, решающих задачи практической степени сложности, необходимо решение задачи построения эффективного алгоритма унификации. При построении алгоритма унификации возникают такие проблемы, как проблема вычисления унификатора и предварительная проверка, являются ли термы унифицированными. Предложенная структура представления термов позволяет отойти от алгоритма унификации, предложенного Дж. Робинсоном Вагин и др., 2004, и разбить этот алгоритм на две основные части. В первой части алгоритма, именуемой ТЕСТ (u, v: терм), проводится предварительная проверка, являются ли термы унифицированными, и, в случае положительного ответа на проверку унифицируемости конкретной позиции, создаются связи множества рассогласований подтермов.

Пример 4. На рисунке 3 представлен результат работы процедуры ТЕСТ (P(y, g(z), f(x)), P(a, x, f(g(y)))):

1) тип связи множества рассогласований {переменная/константа};

2) тип связи - {переменная/функциональный символ};

3) тип связи - {переменная/функциональный символ}.

Размещено на http://www.allbest.ru/

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

Во второй части алгоритма, именуемой УНИФИКАЦИЯ (u, v: терм), строится наиболее общий унификатор пары термов , которые успешно прошли предварительную проверку унифицируемости подтермов, используя информацию о множестве рассогласований, записанной в виде связей.

Пример 5. На рисунке 4 приведен результат работы алгоритма унификации, запрограммированного на Delphi в системе Borland Developer Studio 2006. Данный результат получен при запуске процедуры УНИФИКАЦИЯ (u, v: терм) на множестве пар термов мощностью равной 20.

Размещено на http://www.allbest.ru/

Рис. 4. Результат работы последовательного алгоритма унификации

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

Заключение

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

Список литературы

логика предикат алгоритм

1.Андерсон, 2003 Андерсон Д.А. Дискретная математика и комбинаторика. - М.: Вильямс, 2003.