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

Automatic theorem proving aims at solving mathematical problems with the help of a computer, without human involvement. Proofs of first-order theorems are searched in an infinite space of possible inferences. In these conditions, strategies for finding proofs, in particular the scheme for selecting the next clause to be processed in the proof process, play a decisive role. The paper describes a way to apply genetic algorithms to generate new clause selection schemes by combining the estimation functions and their parameters provided by the prover. An experimental comparison is made between the strategy obtained with the genetic algorithm and the PickGiven5 strategy on the created prover for first-order logic with equality. The strategies were also compared when solving the applied clique problem. The obtained strategy showed good results.

• Применение стратегий оптимизации метода резолюций для компьютерного решения математических задач
  • Введение
  • 1. Автоматический логический вывод
  • 2. Управление поиском
  • 3. Применение генетического алгоритма для получения новых эвристик
  • 4. Программная реализация
  • 5. Проведение экспериментов
  • Заключение
  • Список использованных источников
  • Приложение 1. Список использованных задач
  • Приложение 2. Сравнение стратегий на задачах TPTP
  • Приложение 3. Часть исходного кода