Details
| Title | Применение стратегий оптимизации метода резолюций для компьютерного решения математических задач: выпускная квалификационная работа магистра: направление 02.04.03 «Математическое обеспечение и администрирование информационных систем» ; образовательная программа 02.04.03_01 «Разработка и математическое обеспечение интеллектуальных информационных систем» |
|---|---|
| Creators | Разуваев Данил |
| Scientific adviser | Пак Вадим Геннадьевич |
| Organization | Санкт-Петербургский политехнический университет Петра Великого. Институт компьютерных наук и технологий |
| Imprint | Санкт-Петербург, 2023 |
| Collection | Выпускные квалификационные работы ; Общая коллекция |
| Subjects | стратегии метода резолюций ; генетические алгоритмы ; управление выводом ; автоматическое доказательство теорем ; resolution method strategies ; genetic algorithms ; inference control ; automated theorem proving |
| Document type | Master graduation qualification work |
| File type | |
| Language | Russian |
| Level of education | Master |
| Speciality code (FGOS) | 02.04.03 |
| Speciality group (FGOS) | 020000 - Компьютерные и информационные науки |
| DOI | 10.18720/SPBPU/3/2023/vr/vr23-3936 |
| Rights | Доступ по паролю из сети Интернет (чтение, печать, копирование) |
| Record key | ru\spstu\vkr\25066 |
| Record create date | 8/3/2023 |
Allowed Actions
–
Action 'Read' will be available if you login or access site from another network
Action 'Download' will be available if you login or access site from another network
| Group | Anonymous |
|---|---|
| Network | Internet |
Автоматическое доказательство теорем направлено на решение математических задач при помощи компьютера, без участия человека. Доказательства теорем первого порядка ищутся в бесконечном пространстве возможных выводов. В этих условиях решающую роль играют стратегии поиска доказательств, в частности схема выбора следующей клаузы для обработки в процессе доказательства. В работе описывается способ применения генетических алгоритмов к генерации новых схем выбора клаузы путем комбинации предоставленных прувером оценочных функций и их параметров. Произведено экспериментальное сравнение полученной при помощи генетического алгоритма стратегии со стратегией 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.
| Network | User group | Action |
|---|---|---|
| ILC SPbPU Local Network | All |
|
| Internet | Authorized users SPbPU |
|
| Internet | Anonymous |
|
- Применение стратегий оптимизации метода резолюций для компьютерного решения математических задач
- Введение
- 1. Автоматический логический вывод
- 2. Управление поиском
- 3. Применение генетического алгоритма для получения новых эвристик
- 4. Программная реализация
- 5. Проведение экспериментов
- Заключение
- Список использованных источников
- Приложение 1. Список использованных задач
- Приложение 2. Сравнение стратегий на задачах TPTP
- Приложение 3. Часть исходного кода
Access count: 2
Last 30 days: 0
