WWW.REFERATCENTRAL.ORG.UA - Я ТУТ НАВЧАЮСЬ

... відкритий, безкоштовний архів рефератів, курсових, дипломних робіт

ГоловнаМатематика, Геометрія, Статистика → Методи перевірки тотожності формул числення висловлювань - Курсова робота

Методи перевірки тотожності формул числення висловлювань - Курсова робота

має модель. Коли S1(S2) має модель M, то всяка інтерпретація S, яка включає ?L(L), є моделлю для S. А це суперечить припущенню. Значить S1 v S2 - суперечність. Припустимо тепер, що S1 v S2 - суперечність. Якщо S виконується при деякій інтерпретації, то S має модель M. Коли M включає ?L(L), то M може задовольняти S1(S2), а це суперечить тому, що S1 v S2 не має моделі. Отже, S повинна бути суперечністю. Таким чином, S суперечна тоді і тільки тоді, коли S1 v S2 суперечна.
Теорема доведена.
Метод резолюцій.
Метод резолюцій - це, по суті узагальнення правила одно літерних диз'юнктів Девіса- Патнема.
Розглянемо диз'юнкти виду
C: P,
C': ?P v Q.
Користуючись правилом одно літерних диз'юнктів, із C і C' можна одержати диз'юнкт C'': Q.
Узагальнюючи дане правило і застосовуючи його до будь-якої пари диз'юнктів ( не обов'язково лише одиничних ), одержуємо правило резолюцій.
Правило резолюцій.
Для будь-яких диз'юнктів C і C', якщо існує літера L в C, контрарна літері L' в C', то, викресливши L і L' із C і C' відповідно, побудуємо диз'юнкцію членів, що залишилися. Побудований диз'юнкт називається резольвентою C і C'.
Важливу властивість резольвенти двох диз'юнктів - C1 і C2 - виявляє таке твердження.
Теорема.
Нехай дано два диз'юнкти: C1 і C2. Тоді резольвента C диз'юнктів C1 і C2 - логічний наслідок C1 і C2.
Д о в е д е н н я.
Нехай C1 = L v C1', C2 = ?L v C2', C = C1' v C2', де C1',C2' - диз'юнкції літер. Припустимо, що C1 і C2 виконуються при інтерпретації h. Нехай L хибна в h. Тоді C1 не може бути одиничним диз'юнктом, оскільки C1 була б хибною в h. Отже, C1' повинна виконуватись в h, а тоді і C = C1' v C2' виконується в h. Таким чином, C1' v C2' повинна виконуватись при інтерпретації h. Теорема доведена.
Означення:
Нехай S - множина диз'юнктів. Резолютивним виведенням диз'юнкта C із S називається така скінченна послідовність C1, C2, … , Ck диз'юнктів, в якій кожний із Ci або належить S, або є резольвентою диз'юнктів, що передують Ci, і C = Ck.
Виведення пустого диз'юнкта 0 із S називається доведенням суперечності S, або спростуванням S.
Говорять, що диз'юнкт C може бути виведений або одержаний із S, якщо існує резолютивне виведення C із S.Правило резолюцій - досить потужне правило виведення. Множина диз'юнктів S суперечна тоді і тільки тоді, коли існує резолютивне виведення пустого диз'юнкта 0 із S.
Додаток 1.
Приклад до методу Куайна.
Довести, що формула
P= (((p & q) ? r) & (p ? q)) ? (p ? r) є теоремою числення висловлювань.
Р о з в ' я з о к :
Множина висловлювань формули P є {p, q, …, r}. Вибираємо висловлювання p. При цьому може бути два випадки.
1. p=1. Тоді
P= (((1 & q) ? r) & (1 ? q)) ? (1 ? r) = ((q ? r) & q) ? r = P'.
Вибираємо тепер q і розглядаємо знову можливі випадки:
a1) q=1, тоді P'= ((1 & r) & 1) ? r = r ? r - тавтологія;
a2) q=0, тоді P'= ((0 ? r) & 0) ? r = 0 ? r = 1.
2. p=0. Тоді
P= (((0 & q) ? r) & (0 ? q)) ? (0 ? r) = ((0 ? r) & 1) ? 1 = 1 ? 1 = 1.
Отже, дана формула є тавтологією, а значить, і теоремою числення висловлювань. Крім того, можливі інтерпретації формули r в даній формулі P не відіграють ніякої ролі.
Приклад до методу редукції.
Чи є формула
P = ((p & q) ? r) & (p ? (q ? r)) тавтологією?
Р о з в ' я з о к :
Нехай для деякої інтерпретації h маємо h(P) = 0.
Тоді h(p ? (q ? r)) = 0 і h((p & q) ? r) = 1.
Застосуємо цю ж процедуру до першої з формул.
Одержимо h(p) = 1 і h(q ? r) = 0.
Звідси знаходимо, що h(p) = 1, h(q) = 1 і h(r) = 0, але отримані значення суперечать тому, що h((p & q) ? r) = 1. Одержана суперечність показує, що формула P - тавтологія.
Додаток 2 .
Приклади до методу Девіса-Патнема.
Приклад 1.
Довести, що S = (P v Q v ?R) & (P v ?Q) & ?P & R & U суперечна.
Р о з в ' я з о к :
(P v Q v ?R) & (P v ?Q) & ?P & R & U
(Q v ?R) & (?Q) & R & U - правило 2 з ?P
?R & R & U - правило 2 з ?Q
0 & U - правило 2 з ?R
Оскільки останній диз'юнкт включає пустий диз'юнкт 0, то формула S суперечна.
Приклад 2.
Показати, що S=(P v Q) & ?Q &( ?P v Q v R) несуперечна.
Р о з в ' я з о к :
(P v Q) & ?Q &( ?P v Q v R),
P & (?P v ?R) - правило 2 з ?Q
?R - правило 2 з P
0 - правило 2 з ?R
Остання множина являє собою пустий диз'юнкт. Отже, S несуперечна .
Приклад до методу резолюцій.
Приклад 1 .
Перевірити суперечність множини диз'юнктів S = { P, ?P v Q v R, ?Q v C, ?R v C, ?C }.
Розв'язок
Застосовуючи правило резолюції (ПР) до S, маємо:
(1) P - диз'юнкт 1,
(2) ?P v Q v R - диз'юнкт 2,
(3) ?Q v C - диз'юнкт 3,
(4) ?R v C - диз'юнкт 4,
(5) ?C - диз'юнкт 5,
(6) Q v R за ПР із (1), (2),
(7) ?R за ПР із (4), (5),
(8)апі?Q за ПР із (3), (5),
(9) Q за ПР із (6), (7),
(10) 0 за ПР із (8), (9).
Отже, задана множина диз'юнктів суперечна, оскільки з неї виводиться пустий диз'юнкт.
Додаток 3 .
Приклад до методу резолюцій.
Приклад 2 .
Перевірити суперечність множини диз'юнктів S = { P v Q, P v R, ?Q v ?R, ?P }.
Розв'язок
Застосовуючи ПР до S, маємо:
(1) P v Q - диз'юнкт 1,
(2) P v R - диз'юнкт 2,
(3) ?Q v ?R - диз'юнкт 3,
(4) ?P - диз'юнкт 4,
(5) P v ?R за ПР із (1), (2),
(6) Q за ПР із (1), (4),
(7) P v ?Q за ПР із (2), (3),
(8) R за ПР із (2), (4),
(9) P за ПР із (2), (5),
(10) ?R за ПР із (3), (6),
(11) ?Q за ПР із (3), (8),
(12) ?R за ПР із (4), (5),
(13) ?Q за ПР із (4), (7),
(14) 0 за ПР із (4), (9).
Слід зазначити, що перевірка множини диз'юнктів на суперечність за допомогою правила резолюцій загалом не детермінована, оскільки будувати резольвенти можна різні. З наведеного прикладу видно, що описана стратегія застосування правила резолюцій не є оптимальною. Виведення пустого диз'юнкта з множини S можна було б виконати з меншим числом резольвент, наприклад:
(5) Q за ПР із (1), (4),
(6) R за ПР із (2), (4),
(7) ?Q за ПР із (3), (6),
(8) 0 за ПР із (5), (7).
Висновок:
Дана курсова робота дає можливість краще зрозуміти і вникнути в суть ідей дискретної математики.
Отже, фундаментальною ідеєю щодо відображення реального світу в комп'ютері є ідея дискретизації об'єктів. Для ефективної роботи на комп'ютері необхідно навчитися будувати моделі реальних об'єктів та процесів їх перетворення. Досить часто такими моделями можуть бути конструкції дискретної математики, такі, як алгебра, формула, автомат, граф, алгоритм та інші. Останнім часом завдяки потребам комп'ютерної сфери дискретна математика розвивається досить динамічно. Її розділи поповнюються новими результатами, що виникають від своєрідної взаємодії різних галузей знань, які обслуговують комп'ютери.
Рекомендована література:
1. Мендельсон Е. Введення в математичну логіку. - М.: Мир, 1988. - 320 с.;
2. Новиков П. С. Елементи математичної логіки. - М.: Наука, 1973 - 399 с.;
3. Капітонова Ю. В., Кривий С. Л., Летичевський О. А., Луцький Г. М., Печорін М. К. Основи дискретної математики. - К.: Наукова думка, 2002. - 580 с.
Loading...

 
 

Цікаве