Details

Данная работа посвящена разработке библиотеки на языке Java, предоставляющей API, в которой реализованы следующие алгоритмы унификации: алгоритм Робинсона для унификации пары термов, полиномиальный вариант алгоритма Робинсона, а также линейный алгоритм Патерсона–Вегмана для унификации пары термов. Задачи, решаемые в рамках данной работы: 1. Детализация описания всех вышеупомянутых алгоритмов унификации в виде псевдокода; 2. Реализация представления терма в виде ориентированного ациклического графа; 3. Реализация синтаксического анализатора; 4. Реализация алгоритмов унификации; 5. Проведение тестирования реализованных алгоритмов унификации и сравнение их эффективности между собой. В данной работе приведен обзор существующих программных реализаций алгоритмов унификации. Было отмечено, что некоторые реализации не предоставляют API; некоторые из них плохо задокументированы; некоторые из них не выложены в открытый доступ. В данной работе приведено подробное описание реализованной библиотеки, описан пример взаимодействия с библиотекой. Было осуществлено тестирование библиотеки, сравнение реализованных алгоритмов между собой. Также приведены результаты сравнения данной реализации алгоритма Патерсона–Вегмана с реализацией этого алгоритма в работе de Champeaux.

This work is devoted to the development of a library in the Java language, providing an API, which implements the following unification algorithms: the Robinson algorithm, a polynomial version of the Robinson algorithm and the Paterson-Wegman linear algorithm. The goals of this work are: 1. Detailed description of all the above-mentioned unification algorithms in the form of a pseudocode; 2. Implementation of the representation of the term as a directed acyclic graph; 3. Implementation of a syntax analyzer; 4. Implementation of unification algorithms; 5. Testing the implemented unification algorithms and comparison of their efficiency. In this work the overview of existing software implementations of unification algorithms is given. It was noted that some implementations do not provide APIs; some are poorly documented; some are not publicly available. This work provides a detailed description of the implemented library, provides an example of interaction with the library. The library was tested, the implemented algorithms were compared among themselves. The comparison results of this implementation of the Paterson-Wegman algorithm with the de Champeaux implementation are also given.