разом з єдиним правилом:
(Лат. Modus ponens)
термін середньовічної логіки, що позначає правило виведення і відповідний йому логічний закон.
Теорема правильності обчислення висловлювань стверджує, що всі перераховані вище аксіоми є тавтологія, а за допомогою правила modus ponens з істинних висловлювань можна отримати тільки справжні. Доказ цієї теореми тривіально і зводиться до безпосередньої перевірки. Куди більш цікавим є той факт, що всі інші тавтології можна отримати з аксіом за допомогою правила виведення - це так звана теорема повноти логіки висловлювань.
Логіка предикатів першого порядку
Недоліком логіки висловлювань є її багатослівність - навіть для опису простих завдань потрібна значна кількість логічних змінних і формул. Подання кожного окремого властивості для кожного конкретного об'єкта вимагає окремої логічної змінної, що дуже незручно. Також потрібно використовувати окремі змінні для опису всіх необхідних комбінацій взаємозв'язків між поняттями. З іншого боку, в обчисленні висловлювань кожен атомарний (елементарний) символ позначає вираз деякої довільної складності. При цьому не існує можливості отримати доступ до складових частин цього виразу. Наприклад, фраза «курс долара має тенденцію до зростання», позначена через логічну змінну. говорить тільки про зростання курсу долара і не може бути використана в іншому контексті (дана фраза є релятивно актуальною (замкнутої) сутністю в рамках прагматики розгляду і відповідних синтаксисо-семантичних домовленостей.). Логіка предикатів дозволяє вирішити ці проблеми подання знань.
Головна ідея логіки предикатів полягає у взаимнооднозначное зіставленні кожного унікального об'єкта з індивідуальної об'єктної константою, що позначається ім'ям об'єкта, а клас однотипних об'єктів - з об'єктної змінної, значенням якої є об'єктні константи. Наприклад, вираз, наведене вище, можна уявити на мові логіки предикатів так:
Очевидно, таке уявлення набагато більш наочно і гнучко.
Предикатом називають логічну (висказивательную) функцію, певну на безлічі наборів значень об'єктних змінних. Семантика цієї функції визначається предикатним символом, за яким в дужках йдуть аргументи (об'єктні змінні і константи). Ця функція може приймати тільки два значення: Істина або Брехня, звані істиннісними значеннями. Якщо предикат має тільки один аргумент, то предикатний символ вказує на певну властивість об'єкта, а якщо аргументів кілька - на наявність відносини між об'єктами, представленими аргументами. Відносини між об'єктами середовища, також як і в логіці висловлювань, представляються у вигляді пропозицій (формул), що складаються з змінних, констант, логічних зв'язок, дужок, а також функцій, предикатів і кванторів.
Об'єктна константа або просто константа взаимнооднозначное зіставляється в процесі інтерпретації з будь-яким одним об'єктом середовища і позначається рядком символів, що починаються з великої літери.
Об'єктні змінні або просто змінні позначаються рядком, що починається з малої літери. Областю значень кожної змінної є безліч констант, в загальному випадку нескінченне.
Об'єктні константи і змінні є термами. Як саме вибирати терми для представлення знань - вирішувати розробнику. У наведеному вище прикладі використовувалися константи Долар і Зростає. Введемо змінну. певну на безлічі валют і змінну динаміки зміни курсу. Предикатний символ ізмененіе_курса ставить у взаємно однозначна відповідність будь-якій валюті властивість плаваючого курсу. Функція задає відношення між об'єктом валюта і динамікою зміни. Якщо. то відповідно до тих знаннями що у нас є ( «курс долара має тенденцію до зростання») ізмененіе_курса (Долар, Зростає) = ІСТИНА.
За допомогою предикатів задаються довільні відносини між об'єктами. Предикати починаються з предикатного символу і наступними за ним в дужках упорядкованого набору змінних або констант, відповідних об'єктів, які знаходяться в пойменованому відношенні. Так, наприклад, якщо дві людини Маша і Саша є братом і сестрою, то це ставлення може бути виражено за допомогою предиката
брат_сестра (Маша, Саша).
Предикат може приймати значення Істинно або Брехня. Якщо предикат істини, то відношення має місце, інакше - навпаки.
Якщо деякий об'єкт в точності відповідає безлічі інших, то використовують функції. Наприклад, якщо об'єктами є виконавчі цифри і десяткові цифри, то будь-якого бінарного можна однозначно зіставити десяткове, і висловити це зіставлення у вигляді функції преобразованіе_2_ в_10 (x, y, z). де x, y, z - двійкові числа, а значення функції - десяткове. Вираз преобразованіе_2_ в_10 називають функціональним символом. Функція в логіці предикатів не припускав обов'язкової наявності алгоритму обчислення її значення по аргументам. Вона лише задає за допомогою констант і змінних певне відношення між об'єктами, відповідними її аргументів, і якимось одним об'єктом. Функції також як і змінні або константи є термами.
Вираз предікатний_сімвол (терм, терм, ..., терм) називають атомом. Атом являє предикат. Особливо виділяється атом, предикатним символом якого є знак рівності, а аргументами два терми. Цей атом можна було б представити як рівні (терм, терм) або = (терм, терм). але, як правило, його записують у звичайній інфіксной формі терм = терм. Цей атом правдивий, коли значення обох термів збігаються. Атоми без знака заперечення або зі знаком заперечення називають літералами.
Коли виникає необхідність висловити будь-які властивості, загальні для чималої кількості об'єктів, використовують квантори. У логіці предикатів таких кванторів два:.
Квантор спільності. Сенс квантора спільності збігається з виразом природної мови «для всіх». Тобто, якщо є деяке знання, яке застосовується для будь-якого об'єкта певного типу, то замість перерахування всіх таких об'єктів можна використовувати квантор спільності.
Квантор існування. Якщо виникає необхідність висловити знання про окремий об'єкт з будь-якої сукупності, використовують квантор існування. Квантор існування вимовляється природною мовою як «існує».
Вважають, то квантор пов'язує змінні, які записуються за знаком квантора в дужках. Тому їх називають пов'язаними. Змінні ж, які жоден квантор не пов'язує, називають вільними.
Взаємозв'язок між квантора існування і спільності можна легко виразити за допомогою зв'язки заперечення і вона заснована на такому міркуванні: якщо про будь-який об'єкт із сукупності можна сказати, що він не володіє заданою властивістю, то не існує об'єкта, який володіє цією властивістю. Наприклад, очевидно, що «у будь-який рибки немає рук, значить, не існує рибки, у якій є руки».
Позначимо будь-яку змінну через. а будь-яку формулу, яка містить цю змінну через. тоді справедливі такі закони:
Рівність є атомом особливого типу Терм = Терм або = (Терм, Терм). Рівність означає, що обидва терма в атомі відповідають одному і тому ж об'єкту. Не слід плутати предикат рівності з операцією присвоювання. У наступній таблиці розкрито сенс предиката рівності для різних термів, де X, Y позначають об'єктні константи, x. y - об'єктні змінні, а F (x) - функція:
Синтаксис логіки предикатів дозволяє наочно і просто переходити від природної мови до мови логіки предикатів. Досить правильно ввести відповідні об'єктні константи і предикатні символи, щоб мати можливість коректно описувати стану і явища предметної області. Розглянемо приклад. Припустимо, що наші знання про птахів виражені у вигляді наступних пропозицій:
· Якщо істота має крила, то це істота - птах.
· Якщо істота літає і несе яйця, то це істота - птах.
Алгоритм подання знань на мові логіки предикатів:
1. Виявити. що у фразі є об'єктом, який необхідно зіставити з константою або змінною. Якщо мова йде про конкретний об'єкт, то вводиться константа, якщо ж згадується цілий клас об'єктів, то використовують змінну.
2. Визначити властивості об'єктів. Зіставити властивостями предикатні символи.
3. За допомогою логічних зв'язок сформувати формули констант, змінних і предикатів, відповідних об'єктів і їх властивостей.
Таким чином, на мові логіки предикатів ці знання можуть бути виражені у вигляді формул:
· Імеет_крилья (істота) → птах (істота)
· Літає (істота) несет_яйца (істота) → птах (істота)
В даному прикладі використані одномісні предикати, що мають по одному аргументу. У той же час предикати можуть бути також і багатомісними, тобто мати кілька аргументів. У разі багатомісних предикатів, як вже було зазначено, предикатний символ може розглядатися як деяке загальне властивість об'єктів, що відповідають аргументам, або як відношення, в якому ці об'єкти знаходяться. Варіант першої фрази із застосуванням багатомісного предиката може бути, наприклад, таким:
володіє (істота, крила) → прінадлежіт_к_классу (істота, птиця).
Нами було розглянуто обчислення логіки висловлювань, зокрема класичне числення. Розглянемо відмінності числення предикатів першого порядку від обчислення висловлювань.
Аксіоми числення висловів перетворюються в аксіоми числення предикатів шляхом заміни. тобто логічна змінна замінюється предикатом. Крім того, вводяться дві нові аксіоми:
Безліч правил виведення включає:
· Узагальнений правило Modus Ponens,
і правила введення кванторів
Існують також і некласичні обчислення предикатів першого порядку. Вони можуть будуватися на доповненні безлічі аксіом специфічними для даної предметної області загальнозначущими формулами.
Також можуть додатково використовуватися такі правила виведення:
· Виключення квантора спільності:,
· Виключення квантора існування:,
· Введення квантора існування:.
Тут - довільна формула логіки предикатів, що має пов'язану квантором змінну. - формула. в якій всі входження змінної замінені на константу.
Слід особливо відзначити правило виключення квантора спільності, яке також називають правилом універсального інстанцірованія. Іншими словами суть цього правила можна сформулювати так: якщо будь-яку змінну, що стоїть під квантором спільності в істинному пропозиції замінити будь-яким відповідним термо з області визначення, то результуючі вираз істинний.
Однак, на відміну від логіки висловлювань, логічний висновок в просторі предикатів не так очевидний. Щоб коректно застосовувати правила виведення типу Modus Ponens. система виведення повинна вміти визначати, коли два вирази є еквівалентними, або рівносильними. У численні висловів це тривіально:
два вирази рівносильні тоді і тільки тоді, коли вони синтаксично ідентичні.
У численні предикатів визначення равносильности двох пропозицій ускладнюється наявністю змінних. Оскільки всі терми в логіці предикатів є символьними, то пошук рівносильних пропозицій зводиться до процедури підстановки. що дозволяє замінити терм # 948; на інший терм з безлічі # 952; .
Можливі три види підстановки:
1. Перейменування змінної - замість змінної # 948; підставляється змінна з # 952; .
2. Конкретизація змінної - замість змінної # 948; підставляється константа з # 952 ;.
3. Заміна змінної - замість змінної # 948; підставляється функція з # 952; .
Обов'язковою умовою підстановки є наступну вимогу. В межах області дії підстановки, тобто на множині всіх тих предикатів, до яких вона застосовується, замість однієї і тієї ж змінної # 948; підставляється одна і та ж змінна, константа або функція з # 952; для всіх її входжень # 948 ;. Процес пошуку потрібної підстановки називають також процедурою уніфікації. Підстановка називається найбільш загальної, якщо в результаті її застосування найменше число змінних заміщається константами. Іноді, в правилі Modus Ponens квантори спільності маються на увазі, але не пишуться, тобто замість пишуть просто. а квантори існування взагалі не вживаються. Якщо квантори існування присутні у формулі, то від них слід позбутися, наприклад, за допомогою правила виключення квантора існування. Щоб застосовувати узагальнене правило Modus Ponens. всі формули в постановці завдання повинні бути атомами або імплікації, ліва частина яких є кон'юнкція атомів, а права - атомом або порожнім символом. Такі формули отримали назву хорновскімі пропозиціями. Відповідно, для ефективного виведення в просторі предикатів, необхідно враховувати наведені вище обмеження та вимоги до подання знань.
Проілюструємо роботу правила Modus Ponens в логіці предикатів на простому прикладі. Візьмемо відомий силогізм «всі люди смертні, і Сократ - людина, тому Сократ - смертний». У цій фразі присутні три основних висловлювання - «всі люди смертні», «Сократ - людина» і «Сократ - смертний». Очевидно, необхідно ввести константу «Сократ» і предикатні символи «людина» і «смертний». Тоді фраза «всі люди смертні» на мові логіки предикатів буде виглядати так:
А фраза «Сократ - людина» так:.
Оскільки змінна х пов'язана квантором загальності, то її можна замінити будь-яким значенням з області її визначення, наприклад Сократ. Отже, можна сформувати умову правила Modus Ponens:
а в результаті спрацьовування цього правила приходимо до висновку смертний (Сократ).
Незважаючи на потенційні обчислювальні можливості правила Modus Ponens на практиці воно використовується рідко. В основному через громіздкість обчислень, необхідних для його застосування. Основну частину цих обчислень становить приведення пропозицій до імплікатівной увазі, необхідного для формування умови правила. Більш потужним, легко реалізованим і вимагає менше обчислень є правило резолюції. Це правило лягло в основу парадигми логічного програмування **. використовуваного в багатьох інтелектуальних системах.