Курсова робота на тему: «МЕТОДИ ПЕРЕВІРКИ ТОТОЖНОСТІ ФОРМУЛ ЧИСЛЕННЯ ВИСЛОВЛЮВАНЬ»

Зміст

Вступ    3

1. Теоретична частина:

1.1. Числення висловлення    6

1.2. Алгебраїчний метод    10

1.2.1. Еквівалентні формули числення висловлювань    12

1.3. Метод Куайна    15

1.4. Метод редукції    18

1.5. Метод Девіса-Патнема    18

1.6. Метод резолюцій    22

2. Практична частина:

2.1. Додаток 1    26

2.2. Додаток 2    26

2.3. Додаток 3    27

2.4. Додаток 4    27

2.5. Додаток 5    28

Висновок    31

Список використаної літератури    32

Вступ

Людина здавна прагнула знайти загальну розв’язуючу процедуру доведення теорем. Це бажання чітко простежується у Лейбніца (1646-1716); воно було відроджено Пеано на початку нашого століття і школою Гільберта в 20-х роках. Дуже важлива теорема була доведена Ербраном в 1930 р.: він запропонував автоматичний метод доведення теорем. На жаль, його метод був дуже важкий для реалізації, тому що був досить трудомісткий при ручному обрахунку. З винаходом ЕОМ логіки знову виявили цікавість до автоматичного доведення теорем. У 1960 роки теорема Ербрана була реалізована на ЕОМ Гілмором, а незабаром послідувала більш ефективна процедура, запропонована Девісом і Патнема.

Важливий прогрес в автоматичному доведенні теорем був досягнутий Дж. А. Робінсоном в 1965 р. Він розробив єдине правило виведення – принцип резолюції, що виявився надзвичайно ефективним і легкодоступним для реалізації на ЕОМ. З тих пір було запропоновано багато удосконалень принципу резолюції. Автоматичне доведення теорем додавалося в багатьох областях таких, як аналіз програм, дедуктивні системи відповідей на питання, системи вирішення завдань і технологія роботів. Число додатків продовжує зростати.

Зросла також розуміння важливості самої математичної логіки для дослідників, що працюють в теоретичному програмуванні (computer science). Деяка підготовка в галузі математичної логіки необхідна тепер при читанні статей в багатьох журналах, що відносяться до теоретичного програмування. Однак більшість наявних книг з математичної логікою не орієнтований на теоретичне програмування: майже всі вони призначені для математиків і філософів.

Головними ідеями дискретної математики є :

  1. Ідея подання обчислювальної системи у вигляді системи алгебро-логічних виразів, над якими можна виконувати ряд перетворень, а також у вигляді мережі алгоритмічних модулів.
  2. Ідея алгоритму очевидності, суть якої полягає у створенні спеціалізованої програми для автоматизованої обробки математичних текстів.
  3. Ідея рекурсивної обчислювальної машини нової формації з необмеженим нарощуванням пам’яті та швидкодії.
  4. Ідея створення штучного інтелекту як окремої системи, що визначається своїм розумом, який розміщується в базах знань, і системою перетворень, які динамічно само-організуються.

 

Основним завданням цієї курсової роботи є знаходження і розкриття методів перевірки тотожності формул числення висловлювань, з якими ми стикаємося при розв’язанні інтелектуальних задач, при знаходженні оптимального і швидкого алгоритму розв’язку поставленої задачі.

Об’єктом дослідження є методи перевірки тотожності формул числення висловлювань

Предметом дослідження є алгебро-алгоритмічний підхід до побудови перевірки тотожності формул числення висловлювань.

Актуальність теми. Важливою проблемою сучасного програмування є його математизація, розробка формалізованих мов проектування алгоритмів і програм, а також їх абстрактних моделей. Засоби проектування, аналізу і реалізації алгоритмів є особливо актуальними у зв’язку з важливими процесами комп’ютеризації й автоматизації діяльності суспільства. До таких засобів, зокрема, відносяться алгебри алгоритмів, орієнтовані на вирішення проблем формалізації, обґрунтування правильності, покращення алгоритмів (за обраними критеріями).

Оскільки доведення теорем застосовується у розробці систем штучного інтелекту, то воно автоматично поширюється в різних галузях і включає: ігри; розпізнавання образів; прийняття рішень; адаптивне програмування; створення машинної музики; обробка даних природною мовою; мережі, що навчаються (нейромережі); вербальні концептуальні навчання та ін.

1.1. Числення висловлень

Висловленням будемо називати стверджувальне речення, яке може бути істинним або хибним, але не тим і іншим разом. Приклади висловлень: «Київ – столиця України»; «Цей юнак – студент нашого університету». «Істина» або «хибність», приписані деякому висловленню, називаються істинними значеннями цього висловлення і позначаються 1 і 0 відповідно. Будемо використовувати великі літери (можливо, з індексами) або ланцюжки таких літер для позначення висловлень. З простих висловлювань можна утворювати більш складні висловлювання за допомогою логічних зв’язків. Наприклад, ми можемо позначити висловлення таким чином:

U: «Земля обертається навколо Сонця.»

Q: «Троянда є рослиною.»

P: «Ольга навчається в університеті.»

Символи U, Q, P і т.п., що позначають висловлення, будемо називати атомарними формулами, або атомами. Для побудови складних висловлень у природній мові користуються сполучниками, наприклад: «Зараз іде дощ, і небо захмарене», «Якщо мами немає вдома, то ця дівчинка сумує», «Якщо літо буде спекотним або до нас приїдуть родичі з Сибіру, то ми будемо відпочивати у горах», «Матриця має обернену тоді і тільки тоді, коли її визначник не дорівнює нулю».

У логіці висловлень для побудови з атомарних формул складених виразів будемо використовувати логічні зв’язки: Ø («не»), Ù («та»), Ú («або»), ® («якщо …, то»), « («тоді і тільки тоді, коли»).

Основними логічними операціями є кон`юнкція, диз`юнкція та заперечення.

ЗАВАНТАЖИТИ

Для скачування файлів необхідно або Зареєструватись

Met Perev Totog Formul (316.5 KiB, Завантажень: 1)

Сторінка: 1 2 3 4 5 6
завантаження...
WordPress: 23.29MB | MySQL:26 | 0,608sec