Відкрити головне меню

ВЛВ-резолю́ція (вибіркова лінійна резолюція з визначеними твердженнями), SLD-резолю́ція (англ. SLD-resolution, Selective Linear Definite clause resolution) — це елементарне правило висновування, що застосовується в логічному програмуванні. Воно є вдосконаленням резолюції, що є як правильним, так і спростувально повним для диз'юнктів Горна.

Правило висновування ВЛВРедагувати

Маючи цільове твердження

 

з обраним літералом  , та вхідне визначене твердження

 

чий ствердний літерал (атом)   уніфікується з атомом   обраного літералу  , ВЛВ-резолюція виводить інше цільове твердження, в якому обраний літерал замінюється заперечними літералами вхідного твердження, та застосовується уніфікувальне підставлення  :

 

В найпростішому випадку, в логіці висловлень, атоми   та   є ідентичними, й уніфікувальне підставлення   є виродженим. Проте в загальнішому випадку уніфікувальне підставлення потрібне, щоби зробити ці два літерали ідентичними.

Походження назви «ВЛВ»Редагувати

Назву «ВЛВ-резолюція» (англ. SLD-resolution) було дано Мартеном ван Емденом (англ. Maarten van Emden) безіменному правилу висновування, запропонованому Робертом Ковальським.[1] Його назва походить від ВЛ-резолюції (англ. SL-resolution),[2] що є як правильною, так і повною для необмеженої твердженневої форми логіки. «ВЛВ» відповідає «ВЛ-резолюції з визначеними твердженнями» (англ. SL resolution with Definite clauses).

Як у ВЛ, так і в ВЛВ, «Л» вказує на той факт, що доведення резолюції може бути обмежене лінійною (англ. linear) послідовністю тверджень:

 

де «верхнє твердження»   є вхідним твердженням, а кожне інше твердження   є резольвентою, чиї батьки є попереднім твердженням  . Доведення є спростуванням, якщо останнє твердження   є порожнім твердженням.

У ВЛВ всі твердження в послідовності є цільовими твердженнями, й інше батьківське твердження є вхідним твердженням. У ВЛ-резолюції інше батьківське є або вхідним твердженням, або предковим твердженням раніше в послідовності.

Як у ВЛ, так і в ВЛВ перше «В» вказує на той факт, що єдиним літералом, що розкладається у твердженні  , є той, який однозначно обрано правилом вибору (англ. selection rule) або функцією вибору (англ. selection function). У ВЛ-резолюції літерал, що обирається, обмежено тими, що безпосередньо перед цим було введено до твердження. В найпростішому випадку таку функцію вибору останнім-увійшов-першим-вийшов може бути визначено порядком запису літералів, як у Пролозі. Проте у ВЛВ-резолюції функція вибору є загальнішою, ніж у ВЛ-резолюції та в Пролозі. Тут немає обмеження на вибір літералу.

Обчислювальна інтерпретація ВЛВ-резолюціїРедагувати

В логіці тверджень ВЛВ-спростування показує, що вхідний набір тверджень є нездійсненним. Проте в логічному програмуванні ВЛВ-спростування має також і обчислювальну інтерпретацію. Верхнє твердження   може бути інтерпретовано як заперечення кон'юнкції підцілей  . Виведення твердження   з   є виведенням засобами зворотного виводу нового набору підцілей із застосуванням вхідного твердження як процедури скорочення цілей. Уніфікувальне підставлення   передає як вхід з вибраної підцілі до тіла процедури, так і одночасно вихід з голови процедури до решти невибраних підцілей. Порожнє твердження є просто порожнім набором підцілей, що сигналізує про те, що початкову кон'юнкцію підцілей з верхнього твердження розв'язано.

Стратегії ВЛВ-резолюціїРедагувати

ВЛВ-резолюція неявно визначає дерево пошуку альтернативних обчислень, в якому початкове цільове твердження пов'язується з коренем дерева. Для кожного вузла в цьому дереві, та для кожного визначеного твердження в програмі, чиї ствердні літерали уніфікуються з обраним літералом у цільовому твердженні, пов'язаному з цим вузлом, існує дочірній вузол, пов'язаний з цільовим твердженням, отриманим ВЛВ-резолюцією.

Листовий вузол, що не має дочірніх, є вузлом успіху, якщо пов'язане з ним цільове твердження є порожнім твердженням. Він є вузлом відмови, якщо пов'язане з ним цільове твердження є непорожнім, але його обраний літерал не уніфікується зі ствердним літералом жодного вхідного твердження.

ВЛВ-резолюція є не детерміністською в тому сенсі, що вона не визначає стратегію пошуку для дослідження дерева пошуку. Пролог шукає деревом в глибину, по одній гілці в кожен момент часу, застосовуючи вертання, коли стикається з вузлом відмови. Пошук в глибину є дуже ефективним в його споживанні обчислювальних ресурсів, але він є неповним, якщо простір пошуку містить нескінченні гілки, й стратегія пошуку віддає перевагу пошуку ними перед скінченними гілками: обчислювання не завершується. Можливими є також й інші стратегії пошуку, включно з пошуком в ширину, за першим найкращим та методом гілок і меж. Більше того, пошук може здійснюватися послідовно, одним вузлом в кожен момент часу, або паралельно, багатьма вузлами одночасно.

ВЛВ-резолюція також є не детерміністською в тому згаданому раніше сенсі, що правило вибору визначається не правилом висновування, а окремою процедурою ухвалення рішення, що може бути чутливою до динаміки процесу виконання програми.

Простір пошуку ВЛВ-резолюції є деревом або, в якому різні гілки представляють альтернативні обчислення. У випадку програм логіки висловлень ВЛВ може бути узагальнено так, що простір пошуку стає деревом та–або[en], чиї вузли позначено єдиним літералами, що представляють підцілі, й вузли з'єднано або кон'юнкцією, або диз'юнкцією. В загальному випадку, коли з'єднані підцілі мають спільні змінні, представлення деревом та-або є складнішим.

ПрикладРедагувати

Для заданої логічної програми

q :- p

p

та мети верхнього рівня

q

простір пошуку складається з єдиної гілки, в якій q зводиться до p, яке зводиться до порожнього набору підцілей, сигналізуючи про успішне обчислення. В даному випадку програма є настільки простою, що для функції вибору немає ніякої ролі, і немає потреби в жодному пошуку.

В логіці тверджень ця програма представляється набором тверджень

 

 

а ціль верхнього рівня представляється цільовим твердженням з єдиним заперечним літералом

 

Простір пошуку складається з єдиного спростування

 

де   представляє порожнє твердження.

Якщо до програми додається наступне твердження

q :- r

то в просторі пошуку буде додаткова гілка, чий листовий вузол r є вузлом відмови. В Пролозі, якщо це твердження буде додано на початку оригінальної програми, то для визначення порядку, в якому досліджуватимуться гілки простору пошуку, Пролог використовуватиме порядок, в якому записано твердження. Пролог спробує цю нову гілку першою, зіткнеться з відмовою, потім повернеться до дослідження єдиної гілки оригінальної програми, і досягне успіху.

Якщо тепер до програми буде додано твердження

p :- p

то дерево пошуку міститиме нескінченну гілку. Якщо це твердження буде спробувано першим, то Пролог увійде до нескінченного циклу, й не знайде успішної гілки.

ВЛВЗВРедагувати

ВЛВЗВ (англ. SLDNF)[3] є розширенням ВЛВ-резолюції для поводження із запереченням як відмовою (англ. negation as failure). У ВЛВЗВ цільові твердження можуть містити літерали заперечення як відмови, скажімо, у вигляді  , що можуть обиратися лише тоді, коли вони не містять змінних. Коли обирається такий літерал без змінних, то піддоведення (або підобчислення) намагається визначити, чи існує ВЛВЗВ-спростування, що починається з відповідного не запереченого літералу   як верхнього твердження. Вибрана підціль   досягає успіху, якщо піддоведення відмовляє, і відмовляє, якщо піддоведення досягає успіху.

Див. такожРедагувати

ВиноскиРедагувати

  1. Robert Kowalski Predicate Logic as a Programming Language Memo 70, Department of Artificial Intelligence, Edinburgh University. 1973. Також у Proceedings IFIP Congress, Stockholm, North Holland Publishing Co., 1974, pp. 569—574. (англ.)
  2. Robert Kowalski and Donald Kuehner, Linear Resolution with Selection Function Artificial Intelligence, Vol. 2, 1971, pp. 227-60. (англ.)
  3. Krzysztof Apt and Maarten van Emden, Contributions to the Theory of Logic Programming, Journal of the Association for Computing Machinery. Vol, 1982 — portal.acm.org (англ.)

ДжерелаРедагувати

ПосиланняРедагувати

  • [1] Визначення з Free On-Line Dictionary of Computing (англ.)