МІНІСТЕРСТВО ОСВІТИ І НАУКИ УКРАЇНИ

СХІДНОУКРАЇНСЬКИЙ НАЦІОНАЛЬНИЙ УНІВЕРСИТЕТ

ІМЕНІ ВОЛОДИМИРА ДАЛЯ

ІНСТИТУТ ХІМІЧНИХ ТЕХНОЛОГІЙ

(м. Рубіжне)

ІНЖЕНЕРНО-ЕКОНОМІЧНИЙ ФАКУЛЬТЕТ

КАФЕДРА ВИЩОЇ МАТЕМАТИКИ І КОМП’ЮТЕРНИХ

ТЕХНОЛОГІЙ

ЗАТВЕРДЖУЮ Завідувач кафедри ВМКТ доктор хімічних наук, професор _____________ Кондратов С.О. “.....”................................... 2009 р.

ПОЯСНЮВАЛЬНА ЗАПИСКА

курсової роботи з дисципліни «Програмування»

на тему: «Автоматичний доказ теорем за методом резолюцій»

Виконав студ. гр. ІД-07 __________________________ Кривцун О.О.

^{підпис, число, місяць, рік}

Науковий керівник,

старший викладач __________________________ Хількова Л. О.

^{Оцінка керівника, підпис, число, місяць, рік}

2009

ЗАТВЕРДЖУЮ

Завідувач кафедри ВМКТ

доктор хімічних наук, професор

_____________ Кондратов С.О.

“.....”................................... 2009 р.

ЗАВДАННЯ НА ВИКОНАННЯ РОБОТИ

На тему Автоматичний доказ теорем за методом резолюцій

Вид роботи (курсова, кваліфікаційна, дипломна) - курсова

Виконавець: студент гр. ІД-07 Кривцун О.О. Науковий керівник: старший викладач кафедри ВМКТ Хількова Л.О. Тема і керівник затверджені розпорядженням по кафедрі ВМКТ № ___ від “___”________ 2009 р.

Зміст пояснювальної записки

1. Вступ

2. Теоретична частина

3. Опис алгоритму

4. Приклад роботи

5. Висновки

6. Додатки

Строк здачі роботи на кафедру: не пізніше “___”____________ 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, а не А². Важливим законом є принцип подвійності, згідно якому якщо в деякій справедливій рівності ми замінимо всі входження А на В і В на А, 1 на 0 і 0 на 1, то отримаємо рівність, подвійну першому і також справедливе. Прикладами подвійної рівності є приведені вище аксіоми.

Алгебра Буля широко застосовується при проектуванні і перевірці електричних схем, в яких використовуються реле, що працюють за принципом «так, - ні», при програмуванні і проектуванні ЕОМ, в операціях з перемикачами, сигналами, схемами. У сучасній математичній логіці цей розділ значно вдосконалений і розробляється як теорія булевої алгебри, зокрема як алгебра множин, алгебра висловів і тому подібне В області традиційної логіки співвідношення булевої алгебри часто використовуються для ілюстрації і прояснення відносин між об'ємами понять.