Головна

предикатів.

  1.  Алфавіт логіки предикатів.
  2.  Здійснимість і общезначімость формул логіки предикатів. Теорема Черча.
  3.  Відношення логічного слідування і равносильности на безлічі предикатів. Необхідні і достатні умови.
  4.  Заперечення предиката, його область істинності. Заперечення кон'юнкції і диз'юнкції предикатів.
  5.  Правила виведення в численні предикатів.
  6.  Правила освіти мови в алфавіті (синтаксис) логіки предикатів.

У логіці першого порядку (логіці предикатів) умови ефективного застосування методу резолюцій для доведення теорем такі ж, як і в логіці висловлювань. Нагадуємо, що одна з цих умов - це уявлення теорем в ПКНФ. Правила еквівалентних перетворень формул, введені в логіці висловлювань, рівнозначні і для логіки першого порядку. Однак присутність в формулах кванторів загальності та існування ускладнює застосування теорем до ПКНФ.

У зв'язку з цим додатково вводяться ряд правил, що дозволяють виключити зазначені квантори з формул. Ці правила діляться на дві групи:

1) Правила освіти попереджання нормальних форм (ПНФ);

2) Правила освіти Скулемовскіх стандартних форм (ССФ).

Розглянемо ці форми і правили їх утворення.

Формула F знаходиться в попереджання нормальній формі (ПНФ), тоді і тільки тоді, коли вона має вигляд:

 де кожне  1, n є або  ), Або  , і  є формула, яка містить кванторів.  називається префіксом, а  - Матрицею формули F.

Наприклад, у формулі

префікс  передує матрицю

Розглянемо правила еквівалентних перетворень формул, що містять квантори.

нехай  є формула, яка містить вільну змінну  . Будемо позначати цю формулу  . нехай  є формула, яка не містить змінної  . нехай  є квантор  або квантор  . Тоді правила такі:

1a)

1b)

 2a)

 2b)

3a)

3b)

4a) (

4b)

Використовуючи правила еквівалентних перетворень формул логіки висловлювань і зазначені вісім правил, завжди можна перетворити будь-яку формулу в ПНФ. Розглянемо приклад.

Наведемо формулу  до ПНФ. Використовуючи правило виключення зв'язки імплікації, отримаємо:

.

За правилом 2a маємо:

.

Нарешті, використовуючи правило 3b, отримаємо:

.

Формула в правій частині останнього співвідношення представлена ??в попереджання нормальній формі (ПНФ).

Скулемовская стандартна форма - Це ПНФ, в префікс якої відсутні квантори існування  , А матриця  є наведеної кон'юнктівной нормальною формою (ПКНФ). З цього визначення стає очевидним, що скулемовскіе перетворення формул спрямовані на виключення кванторів існування з попереджання нормальних форм. Розглянемо ці правила перетворення.

нехай формула  знаходиться в попереджання нормальній формі, де  є ПКНФ. Покладемо, що  є квантор існування в префікс .

Якщо ніякої квантор загальності не варто в префікс лівіше  , То виберемо нову константу  , Що відрізняється від інших констант, що входять в  , Замінимо всі  , Що зустрічаються в  , На константу  і викреслимо  з префікса. якщо  - Список всіх кванторів загальності, що зустрічаються лівіше ,  то виберемо новий  місцевий функціональний символ  , Що відрізняється від інших функціональних символів, замінимо всі в  на  і викреслимо  з префікса. Потім цей процес застосовуємо для всіх кванторів існування в префікс; остання з отриманих формул є ССФ - скулемовская стандартна форма. Константи і функції, які використовуються для заміни змінних квантора існування, називають скулемовскімі константами і функціями. Розглянемо приклад.

Отримаємо ССФ для формули:

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

Розглянуті правила еквівалентних перетворень дають можливість уявити будь-яку теорему логіки предикатів в скулемовской стандартній формі. Так як префікс в цій формі містить тільки квантори загальності, то це означає, наприклад, для  що форма отримує значення І, якщо  істинно для кожного  з області  (А в іншому випадку отримує значення Л), то це дає право розглядати  як просте висловлювання і квантор загальності, що зв'язує  , Викреслити з префікса. В рівній мірі цей висновок відноситься і до квантора загальності, що зв'язує інші змінні. Тому для доведення теорем в логіці предикатів можна використовувати тільки матриці, що знаходяться в ПКНФ.

У логіці предикатів доведена також наступна теорема.

нехай  - Безліч диз'юнктів, які представляють ПКНФ в скулемовской стандартній формі деякої формули (теореми)  . тоді формула  суперечлива в тому і тільки в тому випадку, коли безліч  суперечливо.

Механізм застосування методу резолюцій, який використовувався для доведення теорем в логіці висловлювань, може бути застосований і в логіці предикатів. Однак при цьому виникають три істотних питання:

1) як знайти контрарние пари для диз'юнктів, що містять змінні?

2) як обчислити резольвенту з диз'юнктів, що містять змінні?

3) Як отримати максимальну користь з зворотної дедукції з метою підвищення ефективності методу резолюцій?

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

 




 Вступ. |  Алфавіт логіки предикатів. |  Правила освіти мови в алфавіті (синтаксис) логіки предикатів. |  Формулами (семантика мови). |

© um.co.ua - учбові матеріали та реферати