Пошук навчальних матеріалів по назві і опису в нашій базі:

Методичні вказівки до виконання курсової роботи з кредитного модуля „Теорія алгоритмів та математичні основи представлення знань”




462.31 Kb.
НазваМетодичні вказівки до виконання курсової роботи з кредитного модуля „Теорія алгоритмів та математичні основи представлення знань”
Сторінка2/4
Дата конвертації09.10.2012
Розмір462.31 Kb.
ТипМетодичні вказівки
Ав, ba├─ ab
Чиста літера
Визначити істинність формули
1   2   3   4
протиріччям.

Загальнозначущі формули позначаються як і тавтології, тобто ╞A. Схематично співвідношення виконуваних, загальнозначущих формул та протиріч можна представити за допомогою наступної діаграми.




1.5. Числення предикатів

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

Числення предикатів К (теорія першого порядку К) – це аксіоматична теорія, символами якої є:

  • пропозиційні зв’язки , ;

  • квантори загальності  та існування ;

  • допоміжні символи: кома “,”, та дужки “(“, “)”;

  • предметні змінні x1, x2,…;

  • предметні константи a1, a2,…;

  • функціональні символи f1, f 2,…;

  • предикатні символи Р1, Р2,…

Аксіоми числення К розбиваються на логічні аксіоми та власні. Наступні формули є логічними аксіомами числення К.

  1. A (BA);

  2. (A(BC))  ((AB)  (AC));

  3. (BA)  ((BA)  B).

  4. xA(x)  A(y), якщо y вільно для х в формулі А(х).

  5. x(AB(x))  (AxB(x)), якщо А не містить вільних входжень х.

Власні аксіоми формулюються окремо для кожної конкретної предметної області.

Правилами виведення у численні К є наступні:

  1. modus ponens (MP): A, AB ├─B.

  2. правило узагальнення Gen: з Г├─А(х) слідує Г├─xА(х), якщо х не входить вільно в жодну з формул Г.

Як і в численні висловлювань L, наведені аксіоми числення К є не конкретними аксіомами, а схемами аксіом.

Моделлю теорії першого порядку К називається довільна інтерпретація, в якій істинні всі аксіоми теорії К. Якщо правила виведення МР та Gen застосовуються до істинних в даній інтерпретації формул, то результатом є формули, які також істинні в тій самій інтерпретації.

Множина формул, які виводяться за правилами виведення з аксіом теорії К, є теоремами теорії К. Аксіоми А1, А2, А3 теорії К та правило МР визначені в теорії L, відповідно, всі теореми теорії L включаються у множину теорем теорії К.

Теорема 3. Формула, яка отримується із загальнозначущої формули за допомогою правил виведення MP та Gen, є загальнозначущою.

Теорема дедукції в численні К відрізняється від теореми дедукції для числення L. Для формулювання цієї теореми нам потрібні будуть деякі додаткові означення та результати.

Нехай А, В1, ..., Вn – формули числення предикатів. Нехай В1, ..., Вn – це виведення в численні предикатів. Будемо говорити, що формула Ві залежить у виведенні від формули А, якщо виконується одна з умов:

а) Ві є сама формула А і включена у вивід на цій підставі;

б) Ві отримана за одним із правил виведення із попередніх формул, з яких хоча б одна залежить від формули А.

Теорема 4. Нехай Г, А├─ В і при цьому у виводі формула В не залежить від формули А. Тоді Г├─ В.

Теорема 5 (теорема дедукції Ербрана). Якщо Г, А├─ В і при цьому в виводі при застосуванні правила узагальнення Gen до формул, залежних в виводі від А, не зв’язується квантором ніяка вільна змінна формули А, то Г├─ АВ.

Наслідок 1. Якщо Г, А├─ В і при цьому в виводі не використовується правило узагальнення, то Г├─ АВ.

Наслідок 2. Якщо Г, А├─ В і при цьому А замкнена формула, то Г├─ АВ.
1.6. Додаткові правила виведення

При доведенні теорем в численнях висловлювань та предикатів можна використовувати похідні правила введення та видалення зв’язок.

Зв’язка

Введення

Видалення



Г, А ├─ В  Г├─ АВ

А, АВ ├─ В

Г1 ├─ А; Г2 ├─ АВ 

Г1, Г2 ├─ В



Г, А ├─ В; Г, А ├─ В  Г├─ А

А, А├─ В

А ├─ А

&

Г1 ├─ А; Г2 ├─ B 

Г1, Г2 ├─ A&В

Г├─ А&В  Г├─ А

Г├─ А&В  Г├─ B



Г├─ А  Г├─ АB

Г├─ B  Г├─ АB

Г1 ├─ АB; Г2, A├─ C;

Г3, B├─ C  Г1, Г2, Г3 ├─ C



АВ, BA├─ AB

AB ├─ АВ

AB ├─ BA

Нижче наведені правила можна використовувати у логіці предикатів для побудування виведень.

1. Правило універсальної конкретизації (УК):

xA(x) ├─ A(y), якщо y вільно для x в A(x).

2. Правило екзистенціальної конкретизації (ЕК):

xA(x) ├─ A(b), де bD.

3. Правило екзистенціального узагальнення:

A(y) ├─ xA(x), де x вільно для y в A(y).

4. Правило загальності:

C  A(x) ├─ C  xA(x), якщо С не містить вільних входжень x.

5. Правило існування:

A(x)  C├─ xA(x)  C, якщо С не містить вільних входжень x.
1.7. Нормальні форми

Диз’юнктом називається вираз вигляду: A1…An, де A1,…,An – атомарні формули.

Формула А знаходиться у кон’юнктивній нормальній формі (КНФ), якщо вона має вигляд D1&…&Dm, де D1,…,Dm – диз’юнкти. Диз’юнкт, який не містить жодної літери, називається порожнім і позначається □.

Формула А знаходиться у зведеній нормальній форму (ЗНФ), якщо вона має вигляд: (Q1x1)…(Qnxn)M, де кожне Qixi є або xi або xi, а М – формула у кон’юнктивній нормальній формі, яка не містить кванторів. (Q1x1)…(Qnxn) називається префіксом, а М – матриця формули А.

Будь-яку формулу логіки першого порядку можна привести до ЗНФ шляхом послідовного застосування привал де Моргана до операцій диз’юнкції, кон’юнкції та кванторам.

Формула у ЗНФ, яка містить тільки квантори загальності, знаходиться у скулемівській стандартній формі (ССФ). Для приведення формули до ССФ з ЗНФ послідовно застосовують два наступних правила:

1. Якщо квантор існування знаходиться у крайній лівій позиції, то його можна видалити, а змінну, якою він керував, замінити на константу, нову для висхідної формули, у всій формулі.

2. Якщо перед квантором існування стоїть кілька кванторів загальності, то змінна даного квантора у формулі замінюється на новий функціональний символ, який залежить від змінних, які зустрічались перед даним квантором загальності. Потім цей квантор видаляється з префіксу.

Наприклад: А=. Дана формула знаходиться у ЗНФ. Застосуємо правило 1. Замінимо змінну х першого квантора існування на нову константу с. Отримуємо A=. Тепер застосуємо друге правило і замінимо змінну u на новий функціональний символ f від двох змінних: y и z. А=. Такі фіктивні функції називаються скулемівськими функціями.

Виконується наступна теорема.

Теорема 6. Нехай S – ССФ формули А. Тоді А є суперечливою тоді й тільки тоді, коли S суперечлива.

Формула, яка знаходиться у ССФ, можна розглядати як множину диз’юнктів, у яких всі змінні керуються кванторами загальності. Таким чином, якщо формула А суперечлива, то й її множина диз’юнктів також суперечлива, і навпаки.
1.8. Метод Девіса-Патнем

Основна ідея автоматичних методів доведення теорем, які тут розглядаються, полягає в тому, щоби перевірити, чи містить множина диз’юнктів S порожній диз’юнкт □. Якщо S містить □, то множина S невиконувана, якщо ні, то потрібно перевірити, чи може він бути отриманий з даної множини диз’юнктів.

Метод Девіса-Патнем складається з чотирьох правил. На вхід методу подається множина диз’юнктів S і надалі до цієї множини застосовуються послідовно по колу наступні правила.

1. Правило тавтологічних диз’юнктів.

Викреслюємо тавтологічні, тобто абсолютно істинні (логічно істинні) диз’юнкти. Множина диз’юнктів S суперечлива тоді і тільки тоді, коли отримана після викреслювання множина суперечлива. Тобто, якщо суперечлива множина S містить тавтологічний диз’юнкт, то суперечливість її забезпечується не цим диз’юнктом.

2. Правило однолітерних диз’юнктів.

Нехай Di - однолітерний диз’юнкт. Викреслюємо із множини диз’юнктів Di та всі його входження в інші диз’юнкти і отримуємо множину диз’юнктів S’. Якщо множина S’ порожня, то множина диз’юнктів S несуперечлива, в протилежному випадку викреслюємо із S’ всі входження Di. Отримуємо множину диз’юнктів S”. Якщо при отриманні S” якийсь диз’юнкт, з якого викреслили Di, став порожнім, то множина диз’юнктів S суперечлива. Множина диз’юнктів S суперечлива тоді і тільки тоді, коли S” суперечлива.

3. Правило чистих літер.

Чиста літера - це літера множини диз’юнктів, яка не зустрічається у множині диз’юнктів із запереченням.

Викреслюємо із множини диз’юнктів S усі диз’юнкти, які містять в собі чисті літери і отримуємо множину S’. Якщо множина S’ порожня, то множина диз’юнктів S несуперечлива. Множина диз’юнктів S суперечлива тоді і тільки тоді, коли множина S’ суперечлива.

4. Правило розщеплення.

Нехай множина диз’юнктів S має вигляд:

1R)&...&(АnR)&...&(В1R)&...&(BnR)&P, де всі Ai та Bi, залишок Р множини диз’юнктів S не містять жодної з літер R, R. Tоді побудуємо множини S1 та S2 таким чином:

S1: A1&…&An&P

S2: B1&…&Bn&P

Множина диз’юнктів S суперечлива тоді і тільки тоді, коли S1S2 суперечлива, тобто коли одночасно суперечливі множини S1 та S2.
1.9. Правило резолюцій

Правило резолюцій Робінсона є нічим іншим, ніж узагальненням другого правила Девіса-Патнем. Узагальнення полягає в тому, що знімається обмеження в застосуванні другого правила тільки до однолітерних диз’юнктів.

Нехай у висхідній множині диз’юнктів S є два елементи D1 та D2, які мають наступний вигляд:

D1: A1…AnL

D2: B1…BnL

де A1,…,A,B1,…,Bn, L, L - літери, тобто атомарні формули. Тоді диз’юнкт D вигляду

D: A1…An B1…Bn

називається резольвентою D1 та D2. Резольвента D є логічним наслідком диз’юнктів D1 та D2.

Особливим випадком можна вважати, коли диз’юнкти D1 та D2 мають вигляд D1 = L та D2 = L. Тоді їх резольвента D = □, тобто є порожнім диз’юнктом.

Резолютивне виведення з множини диз’юнктів S є послідовність D1, D2,…, Dk така, що кожне Di або належить S, або є резольвентою попередніх Di. Якщо останній диз’юнкт порожній, то множина S є невиконуваною або суперечливою.

У випадку логіки першого порядку, якщо, наприклад, диз’юнкти D1 та D2, мають вигляд D1: L(х) та D2: L(y), то для отримання резольвенти цих двох диз’юнктів нам необхідно їх уніфікувати, тобто замість одних термів підставити інші, щоби отримати однакові літери. Для цього вводиться поняття підстановки.

Підстановка – це скінчена множина вигляду {t1/v1,…, tn/vn}, де всі vi – змінні, а ti – терми відмінні від vi та всі vi різні. Нехай θ = {t1/v1,…, tn/vn} та Е – вираз. Тоді Еθ – вираз, отриманий з Е заміною всіх входжень змінних vi на терм ti для всіх i.

Тепер, коли нам необхідно отримати резольвенту двох диз’юнктів, то можна спробувати скористатись уніфікацією, щоби виділити в них контрарну пару літер (деяку літеру та її заперечення) з точністю до входження термів в ці літери.
2. Приклади розв’язку задач

1. Визначити істинність формули Ф логіки висловлювань за допомогою методу таблиць істинності.

Ф = (C  (C  B))  (A & (BA))

A

B

C

C  B

C  (C  B)

A

BA

(A & (BA))

Ф

F

F

F

T

T

T

F

F

F

F

F

T

F

F

T

F

F

T

F

T

F

T

T

T

T

T

T

F

T

T

T

T

T

T

T

T

T

F

F

T

T

F

T

F

F

T

F

T

F

F

F

T

F

T

T

T

F

T

T

F

T

F

F

T

T

T

T

T

F

T

F

F

Як бачимо, останній стовпець таблиці, який відповідає формулі Ф, містить як істинні значення T, так і хибні F. Отже формула не є тавтологією і не є суперечністю.
2.
1   2   3   4

Схожі:

Методичні вказівки до виконання курсової роботи з кредитного модуля „Теорія алгоритмів та математичні основи представлення знань” icon1 Вимоги до виконання курсової роботи 4 2 Завдання для курсової роботи 7
Дані методичні вказівки призначені для організації виконання курсової роботи студентів спеціальності 000008 «Енергетичний менеджмент»...
Методичні вказівки до виконання курсової роботи з кредитного модуля „Теорія алгоритмів та математичні основи представлення знань” iconМетодичні вказівки до виконання курсової роботи з дисципліни "Податкова система" для студентів напряму 0501 "Економіка і підприємництво"
Методичні вказівки до виконання курсової роботи з дисципліни "Податкова система" / Укладачі: Т. О. Кірсанова, І. М. Кобушко, М. Ю....
Методичні вказівки до виконання курсової роботи з кредитного модуля „Теорія алгоритмів та математичні основи представлення знань” iconТип модуля: обов'язковий Семестр: VI обсяг модуля
Методичні вказівки до виконання курсової роботи для студентів всіх форм навчання та екстернів базових напрямів 050501, 050502, 050504,...
Методичні вказівки до виконання курсової роботи з кредитного модуля „Теорія алгоритмів та математичні основи представлення знань” iconМетодичні вказівки до виконання курсової роботи з дисципліни „ регіональний менеджмент для студентів спеціальності 0306 «Менеджмент І адміністрування»
Методичні вказівки до виконання курсової роботи з дисципліни „Регіональний менеджмент” // Укладачі: А. Ю. Жулавський, О. О. Павленко,...
Методичні вказівки до виконання курсової роботи з кредитного модуля „Теорія алгоритмів та математичні основи представлення знань” iconМетодичні вказівки до виконання курсової роботи Цілі та завдання курсової роботи
Прошу розмістити на сайті дну у розділі «Методичні матеріали для самостійної роботи студентів» наступні матеріали
Методичні вказівки до виконання курсової роботи з кредитного модуля „Теорія алгоритмів та математичні основи представлення знань” iconМетодичні вказівки щодо виконання та оформлення курсової роботи з дисципліни «Обчислювальна математика»
Методичні вказівки з виконання та оформлення курсової роботи з дисципліни «Обчислювальна математика» для студентів геологічного факультету...
Методичні вказівки до виконання курсової роботи з кредитного модуля „Теорія алгоритмів та математичні основи представлення знань” iconРозрахунок та оптимізація характеристик систем електрозв'язку завдання на виконання курсової роботи з дисципліни
Телекомунікації” 0924 передбачене виконання курсової роботи з дисципліни “Теорія електричного зв'язку”. Мета кр закріплення знань...
Методичні вказівки до виконання курсової роботи з кредитного модуля „Теорія алгоритмів та математичні основи представлення знань” iconМетодичні вказівки щодо виконання курсової роботи з курсу „технології програмування розробив: Томашевський В. В
Важливим етапом вивчення дисципліни „ Технології програмування ” є написання курсової роботи. Задачами курсової роботи є
Методичні вказівки до виконання курсової роботи з кредитного модуля „Теорія алгоритмів та математичні основи представлення знань” iconМетодичні вказівки до виконання та оформлення курсової роботи для студентів всіх форм навчання
Методичні вказівки до виконання та оформлення курсової роботи для студентів усіх форм навчання з дисципліни “Програмування”/Укладачі:...
Методичні вказівки до виконання курсової роботи з кредитного модуля „Теорія алгоритмів та математичні основи представлення знань” iconМетодичні вказівки до виконання курсової роботи "Визначення впливу вражаючих факторів нс "
Мармазинський О. А., Савіна О. Ю., Штейн П. В. Методичні вказівки до виконання курсової роботи: “Визначення впливу вражаючих факторів...
Додайте кнопку на своєму сайті:
ua.convdocs.org


База даних захищена авторським правом ©ua.convdocs.org 2014
звернутися до адміністрації
ua.convdocs.org
Реферати
Автореферати
Методички
Документи
Випадковий документ

опубликовать
Головна сторінка