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