Представление и синтаксическая проверка формул языка логики высказываний

Учреждение образования
“БЕЛОРУССКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ
ИНФОРМАТИКИ И РАДИОЭЛЕКТРОНИКИ”

Кафедра интеллектуальных информационных технологий

Отчет по лабораторной работе №1

по курсу «ЛОИС»
на тему: «Представление и синтаксическая проверка формул языка логики высказываний»
Вариант D

Выполнил студент группы
921731:
Проверил:

Эгамшукуров С.Ж

Ивашенко В. П.

МИНСК
2022

Тема

Представление и синтаксическая проверка формул языка логики

высказываний.


Цель

Приобрести навыки программирования алгоритмов синтаксического разбора формул языка логики высказываний.

Вариант D

Проверить является ли формула совершенной конъюнктивной нормальной формой(СДНФ).

СДНФ
Совершенная конъюнктивная нормальная форма (СДНФ) -- это КНФ, удовлетворяющая трем условиям: Не содержит одинаковых элементарных дизъюнкций; Ни одна из дизъюнкций не содержит одинаковых переменных; Каждая элементарная дизъюнкция содержит каждую переменную из входящих в данную КНФ. Любая булева формула, которая не является тождественно истинной, может быть представлена в СДНФ.


Правила построения СДНФ по таблице истинности
Для каждого набора переменных, при котором функция равна 0, записывается сумма, причем переменные, которые имеют значение 1, берутся с отрицанием.


Пример нахождения СДНФ
Записать логическую функцию по ее таблице истинности:



Воспользуемся правилом построения СДНФ:



Получим СДНФ:

Вывод в программе:
Дополнительные теоретические сведения

Грамматика языка логики высказываний.

<константа> ::= 1|0
<символ> ::= A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z
<отрицание> ::= !
<конъюнкция> ::= /\
<дизъюнкция> ::= \/
<импликация> :: = ->
<эквиваленция> ::= ~
<открывающая скобка> ::= (
<закрывающая скобка> ::= )
<бинарная связка> ::= <конъюнкция> | <дизъюнкция> | <импликация> |
<эквиваленция>
<атом> ::= <символ>
<унарная сложная формула> ::= <открывающая скобка><отрицание>
<формула><закрывающая скобка>
<бинарная сложная формула> ::= <открывающая скобка><формула>
<бинарная связка><формула><закрывающая скобка>
<формула> ::= <константа> | <атом> | <унарная сложная формула> |
<бинарная сложная формула>
Программная реализация
В рамках лабораторной работы стандартными средствами языка Java был реализован алгоритм, позволяющий проверить является ли формула СДНФ. Суть алгоритма заключается в первичной проверке формулы, построении дерева выражения и его проверки на соответствие СДНФ.



Рис. 1 – Блок-схема функции Main



Рис. 2 – Блок-схема конструктора класса Handler



Рис. 3 – Блок-схема функции check_used_symbols

Рис. 4 – Блок-схема функции check_brackets



Рис. 5 – Блок-схема конструктора класса ExpressionTree
Примеры выполнения

1. 
   Запись не является СДНФ.
   

Рисунок 6 - Пример работы алгоритма для формулы с ошибкой дублирования элементарной дизъюнкции

2. 
   Запись является СДНФ.
   

Рисунок 7 - Пример работы алгоритма для формулы без ошибок
(((((A\/B)\/C)/\((A\/(!B))\/C))\/(((!A\/B)\/C))/\(((!A)\/(!B))\/C))

3. 
   Запись является СДНФ
   

Рисунок 7 - Пример работы алгоритма для формулы без ошибок

4. 
   Запись не является СДНФ.
   

Рисунок 9 - Пример работы алгоритма для записи, состоящей из пары скобок

5. 
   Запись не является СДНФ.
   

Рисунок 10 - Пример работы алгоритма для пустой записи
Вывод

В ходе выполнения лабораторной работы были приобретены навыки программирования алгоритмов синтаксического разбора формул языка логики высказываний, была разработана программа, позволяющая определить, находится ли формула языка логики высказываний в совершенной конъюнктивной нормальной форме.

Использованные источники

1. 
   Совершенная конъюнктивная нормальная форма — Википедия (wikipedia.org)
   
2. 
   Построение СДНФ и СДНФ по таблице истинности (spravochnick.ru)
   
3. 
   Построение таблицы истинности онлайн | СДНФ | СДНФ | Полином Жегалкина | Таблица истинности булевой функции онлайн | Programforyou
   
4. 
   СДНФ и СДНФ: что это, построение по таблице истинности (fenix.help)