винних) формул. У численні предикатів виведені формули називаються В«теоремамиВ», а послідовність застосованих для їх отримання правил виводу (із зазначенням використовуваних у них формул) - В«доказом теоремиВ». Численні програми обчислення предикатів до ШІ можна тлумачити як методи доведення теорем. p> При доведенні теорем зазвичай використовують процедури спростування. Безліч гіпотез {Hj}, відповідних для доведення теореми, додають до безлічі притаманних галузі експертизи аксіом {Ai}. Потім прагнуть отримати спростування (або прийти до протиріччя), приєднуючи {} - заперечення твердження теореми - до системи {Hj, Ai} і намагаючись довести формулу
.
Ця формула логічно еквівалентна формулі
.
Процедури, що дозволяють будувати докази формул такого типу, називаються В«доказами допомогою спростуванняВ». Вони допомагають уникати менш перспективних напрямків пошуку. Системи доведення теорем в багатьох додатках включають формули логіки предикатів із змінними, пов'язаними кванторами існування. У таких випадках докази дозволяють знаходити конкретизації цих змінних. p> Наприклад, цікаво з'ясувати, чи можна формулу ХС (х) логічно вивести з гіпотез і аксіом. Якщо так, то хотілося б знати конкретизацію для х в термінах виведення. Спроба довести ХС (х) з {Hj, Ai} має бути конструктивною. Проілюструємо подібне доказ таким прикладом. p> Міркування з приводу знань
У більшості зустрічаються в ШІ систем відносяться до галузі експертизи знання діляться на дві категорії: В«фактиВ» і В«правилаВ». Факти - це дані (представлені предикатами), що стосуються галузі експертизи. Наприклад, дані про персонал деякого університету складають безліч фактів. p align="justify"> В· Факт (1)
По-російськи: Жак - професор факультету інформатики.
Логічно: Проф (Інфо, Жак_2).
В· Факт (2).
По-російськи: Марі - студентка математичного факультету,
Логічно: Студ (Мат, Марі-4).
Правила - це дані, представлені за допомогою імплікації або в іншій еквівалентній логічній формі. Вони являють собою узагальнюючі знання про область експертизи. p align="justify"> В· Правило (1)
По-російськи: Якщо y - професор факультету х і w студент (ка) факультету z при x? z, то y може служити зовнішнім екзаменатором для w.
Логічно: Проф (x, y)
Завдання докази (обгрунтування) теореми полягає у встановленні виводимості з фактів і правил якоїсь формули (В«пропозиції-метиВ», В«ув'язненняВ»), що представляє деякий питання.
В· Пропозиція-мета (1).
По-російськи: Чи може Жак служити зовнішнім екзаменатором для Марі?
Логічно: іспит (Жак_2. Марі_4).
Можна застосовувати різні прийоми для вироблення стратегій доведення теореми.
16. Мова Prolog. Терми та об'єкти. Факти та елементарні питання
Терми та об'єкти
У Пролозі об'єкти (тобто елементи) універсуму міркування представляються за допомогою термів так само, як в логіці. У силу того, що мова ці терми НЕ інтерпретує, об'єкти самі є термами - синтаксичними об'єктами одній з наступних категоріях:
В· індивідуальна константи (атоми)
В· змінні
В· функції (функціональні терми), що складаються з імені функції і списку аргументів-термів
Синтаксис розрізняє атоми, змінні і функції. Використовувані угоди згідні конкретним застосуванням. Тут ми використовуємо синтаксис Сі-Прологу. Однак вибір конкретної версії мови Пролог не впливає на відмінність між змінною (ім'ям прозивним) і константою (ім'ям власним). p align="justify"> В· Атом записується трьома способами:
- як ідентифікатор, що починається з малої літери Жаклін генріх_4 (допускається використання підкреслення)
як число 123 1.23
як довільну послідовність символів, розташовану між апострофами Що Ви говорите Більше нічого сказати
В· Змінна - це ідентифікатор, що починається з великої літери Х Ім'я Король_Франціі
В· Функція - це ім'я функції, за яким слідує список термів, поміщених в дужки і розділених комами. Ім'я функції - це нечислової атом. ...
