Page 34 - 6109

4 Логічні моделі та метод резолюцій

4.1 Логічні побудови та логічні моделі

Поняття "логіка" має глибокі філософські корені. Для теорії і практики
штучного інтелекту особливе значення має таке питання: яким чином можна
формалізувати логічні побудови так, щоб вони могли здійснюватися
автоматично, без участі людини.
Як уже зазначалося, логічне виведення за дедукцією (від загальних пра-
вил до часткових наслідків) є одним з основних механізмів мислення, до того ж
цілком бездоганним з погляду логіки.
Можна розглядати, як мінімум, дві задачі пов'язаних з автоматизацією
дедуктивних побудов:
– задача виведення наслідків, яка формулюється так: знайти всі вірно
побудовані формули, які можна логічним шляхом вивести з аксіом на основі
правил виведення; або, у практичнішій інтерпретації - знайти всі наслідки із
заданих фактів;
– задача перевірки справедливості даного твердження. Часто вона тра-
ктується як задача автоматичного доведення теорем і формулюється таким
чином. Дана деяка теорія (логічна модель); потрібно встановити, чи є певне
твердження теоремою, тобто чи можна його вивести з аксіом даної теорії.
Автоматизація дедуктивних побудов знаходить широке практичне за-
стосування, наприклад, в експертних системах. Як ще один приклад можна
згадати програмні системи, які аналізують математичні тексти, написані
спрощеною математичною мовою, та перевіряють правильність доведень, що
містяться у цих текстах.
Механізм автоматичного доведення теорем було покладено в основу
однієї з основних парадигм сучасного програмування – логічного програ-
мування. Програма розглядається як набір логічних формул разом з теоремою,
що має бути доведена. Найвідомішим представником логічного програмування
є мова Пролог.
Логічні моделі є одним з основних засобів завдання знань. Позитивною
характеристикою логічних моделей виступає однозначність теоретичного
обґрунтування і можливість реалізації формально точних логічних побудов;
недоліком − формальний процедурний стиль мислення. Людська логіка −
інтелектуальна модель з нечіткою структурою. У цьому полягає її відмінність
від формальної логіки.
Логічною моделлю називається формальна система, що задається
четвіркою <Т, Р, А, В>. Тут Т – множина базових елементів (алфавіт), Р –
множина синтаксичних правил, на основі яких конструюються правильно
побудовані формули; А – множина аксіом, тобто ті формул, які приймаються
за істинні, В – множина правил виведення.
У рамках логічної моделі істинному твердженню відповідає теорема,
тобто правильно побудована формула, яка може бути виведена з аксіом шляхом
скінченого числа застосувань правил виведення.
Логічні моделі та Продукційні системи основний акцент роблять саме на

34