МІНІСТЕРСТВО ОСВІТИ І НАУКИ УКРАЇНИ
СХІДНОУКРАЇНСЬКИЙ НАЦІОНАЛЬНИЙ УНІВЕРСИТЕТ
ІМЕНІ ВОЛОДИМИРА ДАЛЯ
ІНСТИТУТ ХІМІЧНИХ ТЕХНОЛОГІЙ
(м. Рубіжне)
ІНЖЕНЕРНО-ЕКОНОМІЧНИЙ ФАКУЛЬТЕТ
КАФЕДРА ВИЩОЇ МАТЕМАТИКИ І КОМП’ЮТЕРНИХ
ТЕХНОЛОГІЙ
-
ЗАТВЕРДЖУЮ
Завідувач кафедри ВМКТ
доктор хімічних наук, професор
_____________ Кондратов С.О.
“.....”................................... 2009 р.
ПОЯСНЮВАЛЬНА ЗАПИСКА
курсової роботи з дисципліни «Програмування»
на тему: «Автоматичний доказ теорем за методом резолюцій»
Виконав студ. гр. ІД-07 __________________________ Кривцун О.О.
підпис, число, місяць, рік
Науковий керівник,
старший викладач __________________________ Хількова Л. О.
Оцінка керівника, підпис, число, місяць, рік
2009
ЗАТВЕРДЖУЮ
Завідувач кафедри ВМКТ
доктор хімічних наук, професор
_____________ Кондратов С.О.
“.....”................................... 2009 р.
ЗАВДАННЯ НА ВИКОНАННЯ РОБОТИ
На тему Автоматичний доказ теорем за методом резолюцій
Вид роботи (курсова, кваліфікаційна, дипломна) - курсова
Виконавець: студент гр. ІД-07 Кривцун О.О. Науковий керівник: старший викладач кафедри ВМКТ Хількова Л.О. Тема і керівник затверджені розпорядженням по кафедрі ВМКТ № ___ від “___”________ 2009 р.
Зміст пояснювальної записки
Вступ
Теоретична частина
Опис алгоритму
Приклад роботи
Висновки
Додатки
Строк здачі роботи на кафедру: не пізніше “___”____________ 2009 р.
Завдання видано “____”__________ 2009 р.
Студент ____________________ Кривцун О.О.
(підпис)
Науковий керівник ____________________ Хількова Л.О. (підпис)
КАЛЕНДАРНИЙ ПЛАН
Виконання курсової роботи на тему: Автоматичний доказ теорем за методом резолюцій
№ |
Найменування етапу роботи |
Строк початку |
Строк закінчення |
Відмітка про виконання |
1 |
Підготовка теоретичного матеріалу |
|
12.03.09 |
виконано |
2 |
Розробка стратегії розв’язання задачі |
12.03.09 |
26.03.09 |
виконано |
3 |
Створення блок-схеми |
26.03.09 |
9.04.09 |
виконано |
4 |
Розробка програми розв’язання задачі |
09.04.09 |
30.04.09 |
виконано |
5 |
Створення інтерфейсу користувача |
30.04.09 |
14.05.09 |
виконано |
6 |
Тестування програми |
14.05.09 |
28.05.09 |
виконано |
Студент ____________________ Кривцун О.О.
(підпис)
Науковий керівник ____________________ Хількова Л.О. (підпис)
РЕФЕРАТ
Сторінок 38, ілюстрацій 5, перелік посилань 5 джерел
Об’єкт роботи – автоматичний доказ теорем за методом резолюцій.
Мета роботи – розробка програмного комплексу для реалізації автоматичного доказу теорем за методом резолюцій.
Програмний комплекс розроблено за допомогою середовища програмування Borland C++ Builder. Створений програмний комплекс дозволяє для заданого логічного виразу визначити його істинність або помилковість з поданням всіх проміжних розрахунків при доведенні.
Програму рекомендовано для використання у вищих учбових закладах в якості прикладу автоматичного виконання доказу теорем за методом резолюцій, а також як прикладний інструмент для роботи з доказаннями логічних виразів.
МАТЕМАТИЧНА ЛОГІКА, ЛОГІЧНИЙ ВИРАЗ, МЕТОД РЕЗОЛЮЦІЙ, АКСІОМАТИЧНИЙ ДОКАЗ, АВТОМАТИЧНИЙ ДОКАЗ ТЕОРЕМ
ЗМІСТ
ВСТУП 6
1 ТЕОРЕТИЧНИЙ МАТЕРІАЛ 8
1.1 Булева алгебра 8
1.2 Логіка висловів 9
1.3 Побудова доказів в логіці висловів 11
1.4 Метод резолюцій 15
2 Опис алгоритму 18
3 ПРОГРАМНА РЕАЛІЗАЦІЯ АЛГОРИТМУ 20
3.1 Блок-схема 20
3.2 Мінімальні системні вимоги 21
3.3 Інтерфейс користувача 21
ПЕРЕЛІК ПОСИЛАНЬ 29
RESUME 30
ДОДАТОК А. ЛІСТИНГ ПРОГРАМИ 31
ВСТУП
Основним питанням математичної логіки є питання про алгоритмічну вирішуваність істинності її формул, тобто про доказ істинності логічного виразу на підставі певних правил і законів.
Виходячи з цієї проблеми, предметом даної роботи є автоматичний доказ істинності теорем за допомогою методу резолюцій.
Метою даної роботи є створити програмний комплекс, що реалізовує докази теорем математичної логіки методом, який, на відміну від аксіоматичних методів, з успіхом може бути реалізований на ЕОМ і представлений в зручному для сприйняття вигляді.
Можна виділити наступні завдання, на виконання яких орієнтована дана робота:
а) розробка ефективного алгоритму для реалізації методу резолюцій;
б) програмна реалізація побудованого алгоритму у вигляді програмного комплексу;
в) надання користувачеві проміжних результатів доказу для кращого розуміння і сприйняття методу, додаткової перевірки правильності рішення;
г) оптимізація алгоритму і програмної реалізації для найбільш зручного представлення результатів – результати повинні виводитися у вигляді, максимально наближеному до «ручного» доказу;
д) перевірка адекватності алгоритму і реалізації для різних вхідних даних з різними рівнями складності, особливо важковирішуваних «ручним» шляхом;
е) створення зручного і інтуїтивно зрозумілого інтерфейсу для максимальної зручності користувача.
Із зростанням комп’ютеризованості сучасного життя все більш необхідним стає використання методів математичної логіки для розробки систем і пристроїв. Тому проблема побудови програмних реалізацій трудомістких методів доказу більш ніж актуальна, оскільки спричиняє за собою вдосконалення старих і розробку нових, ефективніших, методів доказу, а також глибше розуміння суті математичних логік і можливості їх застосування.
1 Теоретичний матеріал
1.1 Булева алгебра
Алгебра Буля - історично перший розділ математичної логіки, розроблений ірландським логіком і математиком Дж. Булем в середині XIX ст. Буль застосував методи алгебри для вирішення логічних завдань і сформулював на мові алгебри деякі фундаментальні закони мислення. Буль представляє логіку як алгебру класів (позначатимемо їх символами А, В,...). Основними операціями в даній алгебрі є: складання класів; множення класів; доповнення класу А.
Властивості цих операцій описуються наступними аксіомами:
- асоціативність складання;
- асоціативність множення;
- комунікативність складання;
- комунікативність множення;
- дистрибутивність складання щодо множення;
- дистрибутивність множення щодо складання.
У алгебрі Буля існують два елементи: 0 і 1. Характерна особливість алгебри полягає в тому, що в ній відсутні коефіцієнти і показники ступенів. Сума два А рівна А, а не 2А, як в звичайній алгебрі. Так само і твір два A рівне A, а не А2. Важливим законом є принцип подвійності, згідно якому якщо в деякій справедливій рівності ми замінимо всі входження А на В і В на А, 1 на 0 і 0 на 1, то отримаємо рівність, подвійну першому і також справедливе. Прикладами подвійної рівності є приведені вище аксіоми.
Алгебра Буля широко застосовується при проектуванні і перевірці електричних схем, в яких використовуються реле, що працюють за принципом «так, - ні», при програмуванні і проектуванні ЕОМ, в операціях з перемикачами, сигналами, схемами. У сучасній математичній логіці цей розділ значно вдосконалений і розробляється як теорія булевої алгебри, зокрема як алгебра множин, алгебра висловів і тому подібне В області традиційної логіки співвідношення булевої алгебри часто використовуються для ілюстрації і прояснення відносин між об'ємами понять.