?

Details
Table Card RUSMARC
Title: Исследование эффективности комбинирования алгоритмов унификации со стратегиями оптимизации метода резолюций: выпускная квалификационная работа бакалавра: направление 02.03.03 «Математическое обеспечение и администрирование информационных систем» ; образовательная программа 02.03.03_01 «Интеллектуальные информационные системы и обработка данных»
Creators: Шляга Вячеслав Владимирович
Scientific adviser: Пак Вадим Геннадьевич
Organization: Санкт-Петербургский политехнический университет Петра Великого. Институт компьютерных наук и технологий
Imprint: Санкт-Петербург, 2022
Collection: Выпускные квалификационные работы; Общая коллекция
Subjects: метод резолюций; автоматическое доказательство теорем; стратегия оптимизации; алгоритм уни­фикации; resolution rule; automated logic reasoning; optimization strategies; unification algorithms
Document type: Bachelor graduation qualification work
File type: PDF
Language: Russian
Level of education: Bachelor
Speciality code (FGOS): 02.03.03
Speciality group (FGOS): 020000 - Компьютерные и информационные науки
DOI: 10.18720/SPBPU/3/2022/vr/vr22-3052
Rights: Доступ по паролю из сети Интернет (чтение, печать, копирование)
Additionally: New arrival
Record key: ru\spstu\vkr\19763

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

Annotation

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

The subject of the graduate qualification work is «Research of the efficiency of combining unification algorithms and resolution method’s optimization strategies». This work belongs to the field of automated logical reasoning and is about the efficiency of unification algorithms and optimizations strategies in resolution method. The first chapter basically describes first-order logic, resolution method and modern automated reasoning systems. The second chapter describes formula preparation for resolution method, chosen unification algorithms and optimization strategies. The third chapter describes developed automated reasoning system with unification algorithms and optimization strategies in it. The forth chapter is about testing developed system and comparing optimization strategies and unification algorithms. Based on the result of the research, conclusions about the efficiency of unification algorithms and optimizations strategies are made.

Document access rights

Network User group Action
ILC SPbPU Local Network All Read Print Download
External organizations N2 All Read
External organizations N1 All
Internet Authorized users SPbPU Read Print Download
Internet Authorized users (not from SPbPU, N2) Read
Internet Authorized users (not from SPbPU, N1)
-> Internet Anonymous

Table of Contents

  • Исследование эффективности комбинирования алгоритмов унификации со стратегиями оптимизации метода резолюции
    • Введение
    • 1. Автоматическое доказательство теорем в логике предикатов первого порядка
    • 2. Метод резолюций
    • 3. Программная реализация
    • 4. Тестирование
    • Заключение
    • Список сокращений и условных обозначений
    • Список использованных источников
    • Приложение 1. Псевдокод алгоритма Робинсона
    • Приложение 2. Псевдокод модифицированного алгоритма унификации HERE
    • Приложение 3. Программная реализация метода резолюции
    • Приложение 4. Программная реализация алгоритма унификации Робинсона
    • Приложение 5. Программная реализация алгоритма унификации Мартелли-Монтанари
    • Приложение 6. Программная реализация метода насыщения уровня
    • Приложение 7. Программная реализация стратегии предпочтения более коротких дизъюнктов
    • Приложение 8. Программная реализация метода стратегии вычеркивания
    • Приложение 9. Программное представление формул логики первого порядка

Usage statistics

stat Access count: 0
Last 30 days: 0
Detailed usage statistics