ВЛВ-резолюція

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

${\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}$

з обраним літералом ${\displaystyle \neg L_{i}}$, та вхідне визначене твердження

${\displaystyle L\lor \neg K_{1}\lor \cdots \lor \neg K_{m}}$

чий ствердний літерал (атом) ${\displaystyle L\,}$ уніфікується з атомом ${\displaystyle L_{i}\,}$ обраного літералу ${\displaystyle \neg L_{i}\,}$, ВЛВ-резолюція виводить інше цільове твердження, в якому обраний літерал замінюється заперечними літералами вхідного твердження, та застосовується уніфікувальне підставлення ${\displaystyle \theta \,}$:

${\displaystyle (\neg L_{1}\lor \cdots \lor \neg K_{1}\lor \cdots \lor \neg K_{m}\ \lor \cdots \lor \neg L_{n})\theta }$

В найпростішому випадку, в логіці висловлень, атоми ${\displaystyle L_{i}\,}$ та ${\displaystyle L\,}$ є ідентичними, й уніфікувальне підставлення ${\displaystyle \theta \,}$ є виродженим. Проте в загальнішому випадку уніфікувальне підставлення потрібне, щоби зробити ці два літерали ідентичними.

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

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

${\displaystyle C_{1},C_{2},\cdots ,C_{l}}$

де «верхнє твердження» ${\displaystyle C_{1}\,}$ є вхідним твердженням, а кожне інше твердження ${\displaystyle C_{i+1}\,}$ є резольвентою, чиї батьки є попереднім твердженням ${\displaystyle C_{i}\,}$. Доведення є спростуванням, якщо останнє твердження ${\displaystyle C_{l}\,}$ є порожнім твердженням.

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

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

В логіці тверджень ВЛВ-спростування показує, що вхідний набір тверджень є нездійсненним. Проте в логічному програмуванні ВЛВ-спростування має також і обчислювальну інтерпретацію. Верхнє твердження ${\displaystyle \neg L_{1}\lor \cdots \lor \neg L_{i}\lor \cdots \lor \neg L_{n}}$ може бути інтерпретовано як заперечення кон'юнкції підцілей ${\displaystyle L_{1}\land \cdots \land L_{i}\land \cdots \land L_{n}}$. Виведення твердження ${\displaystyle C_{i+1}\,}$ з ${\displaystyle C_{i}\,}$ є виведенням засобами зворотного виводу нового набору підцілей із застосуванням вхідного твердження як процедури скорочення цілей. Уніфікувальне підставлення ${\displaystyle \theta \,}$ передає як вхід з вибраної підцілі до тіла процедури, так і одночасно вихід з голови процедури до решти невибраних підцілей. Порожнє твердження є просто порожнім набором підцілей, що сигналізує про те, що початкову кон'юнкцію підцілей з верхнього твердження розв'язано.

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

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

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

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

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

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

q :- p

p

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

q

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

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

${\displaystyle q\lor \neg p}$

${\displaystyle p\,}$

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

${\displaystyle \neg q}$

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

${\displaystyle \neg q,\neg p,{\mathit {false}}}$

де ${\displaystyle {\mathit {false}}\,}$ представляє порожнє твердження.

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

q :- r

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

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

p :- p

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

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

• Джон Алан Робінсон

• Jean Gallier, SLD-Resolution and Logic Programming chapter 9 of Logic for Computer Science: Foundations of Automatic Theorem Proving, онлайнова редакція 2003 року (вільна для завантаження), початково опублікована Wiley в 1986 році (англ.)
• John C. Shepherdson, SLDNF-Resolution with Equality, Journal of Automated Reasoning 8: 297—306, 1992; визначає семантики, по відношенню до яких SLDNF-резолюція з еквівалентністю є правильною та повною (англ.)

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