Метод резолюцій
Правила у логічному програмуванні.
Логічне програмування.
Пролог і логічне програмування.
1.Логическое програмування - це напрям у програмуванні, заснований на ідеях та методах математичної логіки. Термін логічне програмування в літературі з інформатики трактується у широкому та вузькому значенні.
У широкому тлумаченні ЛП включає коло понять, методів, мов та систем, в основі якого лежить ідея опису задачі з сукупністю тверджень деякою логічною мовою та отримання рішення задачі шляхом побудови логічного висновку в деякій формальній дедуктивній системі. Класи формул, що використовуються для опису задач, методи виведення та моделі обчислень, що використовуються для опису задач, методи виведення та моделі обчислень, що використовуються в таких системах, дуже різноманітні, тому різні їх комбінації утворюють специфічні стилі програмування: концептуальна, функціональна (аплікативна) та ін. .
Найбільші практичні результати досягнуто в системах програмування, де як логічні програми використовуються спеціальні класи логічних формул: хорнівські диз'юнкти, а як спосіб їх використання застосовуються спеціальні методи логічного висновку-варіантиметоду резолюції.
Програмування з використанням таких систем називаєтьсяхорновським або резолюційним, але найчастіше -логічним програмуванням, переносячи вузьке трактування терміна на ширше поняття.
Найвідомішими системами такого роду є реалізації мови Prolog (програмування в термінах логіки – Programming in logic). Розглянемо основні ідеї та поняття ЛП у вузькому значенні.
Неформально логічна програма описуєбезліч об'єктів, безліч функцій та відношення цих об'єктів. Будується логічна програма як набір тверджень про об'єкти, функції та відносини. Такий опис є статистичним і жодного обчислювального процесу задає, тобто. можна вважати, що цей опис визначає БД у якій зберігаються об'єкти та задані на них функції та відносини, наприклад, у вигляді графіків. До конкретного застосування логічної програми відноситься поняття запиту (мети) - наприклад, яке значення функції заданої логічної програмою при даному значенні аргументу. Обчислення відповіді запит відповідає доказу існування такого об'єкта. Провалу, якими проводяться обчислення, утворюють процедурно-операційну семантику логічної програми. Успіхи мови Prolog обумовлені тим, що з одного боку, за допомогою логічних формул хорнівських диз'юнктів, що використовуються в них, - можна описати багато практичних завдань, а з іншого - знайдено простоту інтерпретації цих формул і побудовано досить ефективну реалізацію системи ЛП.
2.Правила у Prolog мають вигляд:
m
де , - Це атоми, атом називається заголовком, а атоми - тілом правила. Тіло може бути порожнім (при m=0)- такі правила називаютьсяфактами. Атом має вигляд
Де - арний предикатний символ чи ім'я відношення; - Терми.
Терм - це або ім'я змінної, або константа, або складовий терм вигляду f - це n-арний функціональний символ.
Функції, що задаються при логічному програмуванні, представляються як відносин - n-місцева функція у =f (X1,X2…Xn) представляється як (n+1)- місцевого відносини виду F(X1,X2…Xn,Y).
Запит (це мета) має вигляд: С1, С2. Сr, де r>= 0 іС1, C2…Сr- атоми.
Кожне правило допускає логічну тапроцедурну інтерпретацію (у семантиці). Логічна інтерпретація правила-«істинність A0 випливає з істинності а1 і істинності A2, і істинності Аm» або «Ао істинно, якщо істинні А1, A2, Am».
Т.о. правила розглядаються як формули мови логіки предикатів виду:
Тут – квантор спільності.
- логічна зв'язка "І".
- логічна зв'язка «якщо, то»
У Пролозі дані формули записуються в зворотний бік і використовуються інші позначення:
- позначається "," (комою) або словом and . v - ";" (точка з комою) або "оr".
- "I" або ": -" або if.
Формула з використанням зв'язок логіч. програм. може бути перетворена в еквівалентну, але має зв'язки (НЕ) і (АБО) формулу виду:
(т0).
Такі формули називаються хорновськими диз'юнкціями, а стиль програмування хорновським.
3.Метод резолюції - отримавши на вхід логічну програму з приєднаними до неї запитами у вигляді безлічі хорнівських диз'юнктів, намагається побудувати виведення порожнього диз'юнкту, що позначається символом "а". Якщо це йому вдається, тоді мета допускається, інакше відкидається. Реалізується метод резолюції та допомогою двох правил:
Правило резолюції або правило склеювання, яке під час роботи викликає процедуру уніфікації - зіставлення.
Уніфікація - це процес, на вхід якого надходить два терми і для них знаходиться уніфікатор.
Уніфікатором двох термів називається підстановка, яка робить терми однаковими і якщо уніфікатор існує, то терми називаються уніфікованими і для них відшукується найбільш загальний уніфікатор, якщо ні - процедура уніфікації повідомляє про відмову.
Правило резолюції. Дозволяє з диз'юнктів:
Отримати новийдиз'юнкт:
Тут-найбільш загальний уніфікатор термів t і s забезпечує їх рівність і означає, що всі підстановки уніфікатора виконані для всіх атомів, що входять в диз'юнкти D1і D2. Диз'юнкти D1 і D2 називаються батьками диз'юнкту D. У диз'юнкті D відсутня пара
, при цьому ()=() і пара є тавтологією (тотожно істинною) і може бути видалена з подальших обчислень і виконує правило резолюції.
Правило склеювання дозволяє з диз'юнкту A(t)A(s)отримати диз'юнкт, тобто. здійснюється склеювання однакових атомів, отриманих після уніфікуючої підстановки.
Робота в системі програмування Turbo Prolog.