Введение 3
1 Описание истории вопроса 5
2 Изложение основных технических инструментов необходимых для работы 8
2.1 Основные инструменты классической логики высказываний 8
2.2 Основные инструменты модальной логики 9
2.3 Семантика Крипке 11
2.4 Метод фильтрации 13
2.5 Техника прореживания 16
2.6 Доказательство разрешимости 18
3 Описание предметных областей и задач, предполагаемых к решению 21
4 Выполнение моделирования задач на языке математической логики 24
4.1 Задача про веб-сайт 24
4.2 Задача по теории игр 26
4.3 Задача по временной логике 27
5 Нахождение разрешающих алгоритмов 28
5.1 Задача про веб-сайт 28
5.2 Задача по теории игр 29
5.3 Задача по временной логике 30
Заключение 32
Список использованных источников 33
Модальная логика является разделом математической логики, изучающей «модальные» логические связки, такие как «необходимо» и «возможно». То есть, она изучает не только утверждения и отрицания, но и так называемые сильные и слабые утверждения и отрицания. К сильным относится, к примеру, утверждение «Это необходимо истинно», а к слабым относится «Это возможно ложно».
Интерес к модальной логике считается высоким, что связано с широким разнообразием прикладного применения модальностей. Модальная логика в частности помогает решать вопросы, которые касаются обучения искусственного интеллекта, теории игр, анализа достоверности и доступа к информации, а также к изменению состояния объектов в пространстве и во времени. И это только малая часть вопросов, ответ на которые ищут при помощи модальной логики.
Модальная логика и её прикладные приложения математически активно исследовались К.Льюисом [1], К. Геделем, Д. Леммоном [2,3,4], Д. Скотт [4], Р. Фейсом [5], В. В. Рыбаковым [6] и другими авторами.
Цель бакалаврской работы - построить оптимальный алгоритм распознающий выполнимость формулы. Освоить техники, которые позволят при работе с модальной системой упростить нахождение доказательства разрешимости.
На основе условии может применяться как метод фильтрации, так и техника прореживания.
Метод фильтрации объединяет все узлы, которые при доказательстве разрешимости, имеют практически идентичный процесс и результат доказательства. В результате чего при доказательстве «отфильтрованного» узла одновременно доказываются все узлы, которые в этот самый узел и вошли. Что ускоряет и упрощает дальнейшее доказательство того что система является финитно-аппроксимируемой, а затем и того что она разрешима.
Техника прореживания позволяет избавиться от таких узлов, которые могут являться лишними при проверке формулы, что также упрощает и ускоряет проверку разрешающего алгоритма.
В работе получены следующие результаты:
1. благодаря использованию техники прореживания был получен максимально быстрый алгоритм проверки доступности веб-сайта, который при всем при этом не нарушает связность алгоритма проверки;
2. используя метод фильтрации, мы смогли распределить большое число вероятных событии в несколько групп, что значительно облегчает процесс анализа поведения, и нахождения выполнимости формулы;
3. использование данных техник в комбинации позволяет максимально упростить проверку различных состоянии, что максимально сокращает время и сложность алгоритма распознавания выполнимости.
Полученные результаты имеют прикладное значение и могут быть с некоторыми изменениями использованы во многих сферах жизни, что можно назвать значимым вкладом в исследования по приложениям математики к информационным технологиям.
