Детальная информация

Данная работа посвящена разработке библиотеки на языке 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.

• ВВЕДЕНИЕ
• БАЗОВЫЕ ОПРЕДЕЛЕНИЯ ТЕОРИИ УНИФИКАЦИИ
  • Язык термов логики первого порядка
  • Подстановка
  • Композиция подстановок
  • Унификатор множества термов
• ОБЗОР СУЩЕСТВУЮЩИХ ПРОГРАММНЫХ РЕАЛИЗАЦИЙ АЛГОРИТМОВ УНИФИКАЦИИ
  • Vampire
  • Coq
  • E Theorem Prover
  • SPASS
  • Реализация на языке Haskell
  • ACL2
  • Реализации алгоритмов унификации на языке Pascal
  • Реализации алгоритмов унификации на языке Pascal, описанные Martelli и Montanari
  • Реализации алгоритмов унификации на языке Java
• ОПИСАНИЕ АЛГОРИТМОВ УНИФИКАЦИИ
  • Алгоритм Робинсона для унификации множества термов
  • Алгоритм Робинсона для унификации пары термов посредством рекурсивного спуска
  • Полиномиальный вариант алгоритма Робинсона для унификации пары термов
  • Линейный алгоритм Патерсона–Вегмана для унификации пары термов
  • Преобразование упорядоченной подстановки в неупорядоченную подстановку
• ПРОГРАММНАЯ РЕАЛИЗАЦИЯ АЛГОРИТМА УНИФИКАЦИИ
  • Общая структура API
    • Пакет syntax
    • Пакет unification
  • Представление термов
  • Синтаксический анализатор
  • Детализация реализаций алгоритмов унификации
    • Подстановка
    • Унификация
  • Пример использования библиотеки
• ТЕСТИРОВАНИЕ РЕАЛИЗОВАННЫХ АЛГОРИТМОВ УНИФИКАЦИИ
  • Описание процесса тестирования
  • Результаты тестирования
  • Сравнение с реализацией de Champeaux
• ЗАКЛЮЧЕНИЕ
• СПИСОК ИСПОЛЬЗОВАННОЙ ЛИТЕРАТУРЫ