Детальная информация
Название | Многопоточный обратный метод Маслова: выпускная квалификационная работа магистра: направление 02.04.03 «Математическое обеспечение и администрирование информационных систем» ; образовательная программа 02.04.03_01 «Разработка и математическое обеспечение интеллектуальных информационных систем» |
---|---|
Авторы | Шляга Вячеслав Владимирович |
Научный руководитель | Пак Вадим Геннадьевич |
Организация | Санкт-Петербургский политехнический университет Петра Великого. Институт компьютерных наук и кибербезопасности |
Выходные сведения | Санкт-Петербург, 2024 |
Коллекция | Выпускные квалификационные работы; Общая коллекция |
Тематика | обратный метод Маслова; автоматическое доказательство теорем; параллельные алгоритмы; inverse proving method; automated theorem proving; parallel algorithms |
Тип документа | Выпускная квалификационная работа магистра |
Тип файла | |
Язык | Русский |
Уровень высшего образования | Магистратура |
Код специальности ФГОС | 02.04.03 |
Группа специальностей ФГОС | 020000 - Компьютерные и информационные науки |
DOI | 10.18720/SPBPU/3/2024/vr/vr24-3916 |
Права доступа | Доступ по паролю из сети Интернет (чтение, печать, копирование) |
Дополнительно | Новинка |
Ключ записи | ru\spstu\vkr\33135 |
Дата создания записи | 29.08.2024 |
Разрешенные действия
–
Действие 'Прочитать' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети
Действие 'Загрузить' будет доступно, если вы выполните вход в систему или будете работать с сайтом на компьютере в другой сети
Группа | Анонимные пользователи |
---|---|
Сеть | Интернет |
Данная работа посвящена улучшению производительности алгоритма обратного метода Маслова с помощью утилизации многопоточной среды. Предлагаемая модель использует несколько запущенных программ, каждая из которых является отдельным прувером, запущенным с уникальной настройкой эвристик. Для повышения производительности они обмениваются промежуточными данными между друг другом.
This article introduces a novel multiprocessing methodology tailored for the Inverse Method, a critical component of Automated Theorem Provers (ATPs), aimed at optimizing theorem proving efficiency. Our approach utilizes multiple running units, each operating as a distinct prover equipped with specific heuristic options, collaborating to explore conjectures and verify theorems. Central to our methodology is the integration of shared memory, enabling seamless communication and data exchange among the processing units, facilitating collaborative problem-solving. We delve into the implementation details of our multiprocessing prover, highlighting the incorporation of heuristic options customized to diverse problem domains and efficient memory sharing mechanisms for formulas. Through rigorous experimentation and benchmarking across various theorem proving tasks, we evaluate the performance and scalability of our approach.
Место доступа | Группа пользователей | Действие |
---|---|---|
Локальная сеть ИБК СПбПУ | Все |
|
Интернет | Авторизованные пользователи СПбПУ |
|
Интернет | Анонимные пользователи |
|
Количество обращений: 0
За последние 30 дней: 0