ВЛВ-резолю́ція (вибіркова лінійна резолюція з визначеними твердженнями), SLD-резолю́ція (англ. SLD-resolution, Selective Linear Definite clause resolution) — це елементарне правило висновування, що застосовується в логічному програмуванні. Воно є вдосконаленням резолюції, що є як правильним, так і спростувально повним для диз'юнктів Горна.
Правило висновування ВЛВ
Маючи цільове твердження
з обраним літералом , та вхідне визначене твердження
чий ствердний літерал (атом) уніфікується з атомом обраного літералу , ВЛВ-резолюція виводить інше цільове твердження, в якому обраний літерал замінюється заперечними літералами вхідного твердження, та застосовується уніфікувальне підставлення :
В найпростішому випадку, в логіці висловлень, атоми та є ідентичними, й уніфікувальне підставлення є виродженим. Проте в загальнішому випадку уніфікувальне підставлення потрібне, щоби зробити ці два літерали ідентичними.
Походження назви «ВЛВ»
Назву «ВЛВ-резолюція» (англ. SLD-resolution) було дано Мартеном ван Емденом (англ. Maarten van Emden) безіменному правилу висновування, запропонованому Робертом Ковальським. Його назва походить від ВЛ-резолюції (англ. SL-resolution), що є як правильною, так і повною для необмеженої твердженневої форми логіки. «ВЛВ» відповідає «ВЛ-резолюції з визначеними твердженнями» (англ. SL resolution with Definite clauses).
Як у ВЛ, так і в ВЛВ, «Л» вказує на той факт, що доведення резолюції може бути обмежене лінійною (англ. linear) послідовністю тверджень:
де «верхнє твердження» є вхідним твердженням, а кожне інше твердження є резольвентою, чиї батьки є попереднім твердженням . Доведення є спростуванням, якщо останнє твердження є порожнім твердженням.
У ВЛВ всі твердження в послідовності є цільовими твердженнями, й інше батьківське твердження є вхідним твердженням. У ВЛ-резолюції інше батьківське є або вхідним твердженням, або предковим твердженням раніше в послідовності.
Як у ВЛ, так і в ВЛВ перше «В» вказує на той факт, що єдиним літералом, що розкладається у твердженні , є той, який однозначно обрано правилом вибору (англ. selection rule) або функцією вибору (англ. selection function). У ВЛ-резолюції літерал, що обирається, обмежено тими, що безпосередньо перед цим було введено до твердження. В найпростішому випадку таку функцію вибору останнім-увійшов-першим-вийшов може бути визначено порядком запису літералів, як у Пролозі. Проте у ВЛВ-резолюції функція вибору є загальнішою, ніж у ВЛ-резолюції та в Пролозі. Тут немає обмеження на вибір літералу.
Обчислювальна інтерпретація ВЛВ-резолюції
В логіці тверджень ВЛВ-спростування показує, що вхідний набір тверджень є нездійсненним. Проте в логічному програмуванні ВЛВ-спростування має також і обчислювальну інтерпретацію. Верхнє твердження може бути інтерпретовано як заперечення кон'юнкції підцілей . Виведення твердження з є виведенням засобами зворотного виводу нового набору підцілей із застосуванням вхідного твердження як процедури скорочення цілей. Уніфікувальне підставлення передає як вхід з вибраної підцілі до тіла процедури, так і одночасно вихід з голови процедури до решти невибраних підцілей. Порожнє твердження є просто порожнім набором підцілей, що сигналізує про те, що початкову кон'юнкцію підцілей з верхнього твердження розв'язано.
Стратегії ВЛВ-резолюції
ВЛВ-резолюція неявно визначає дерево пошуку альтернативних обчислень, в якому початкове цільове твердження пов'язується з коренем дерева. Для кожного вузла в цьому дереві, та для кожного визначеного твердження в програмі, чиї ствердні літерали уніфікуються з обраним літералом у цільовому твердженні, пов'язаному з цим вузлом, існує дочірній вузол, пов'язаний з цільовим твердженням, отриманим ВЛВ-резолюцією.
Листовий вузол, що не має дочірніх, є вузлом успіху, якщо пов'язане з ним цільове твердження є порожнім твердженням. Він є вузлом відмови, якщо пов'язане з ним цільове твердження є непорожнім, але його обраний літерал не уніфікується зі ствердним літералом жодного вхідного твердження.
ВЛВ-резолюція є не детерміністською в тому сенсі, що вона не визначає стратегію пошуку для дослідження дерева пошуку. Пролог шукає деревом в глибину, по одній гілці в кожен момент часу, застосовуючи вертання, коли стикається з вузлом відмови. Пошук в глибину є дуже ефективним в його споживанні обчислювальних ресурсів, але він є неповним, якщо простір пошуку містить нескінченні гілки, й стратегія пошуку віддає перевагу пошуку ними перед скінченними гілками: обчислювання не завершується. Можливими є також й інші стратегії пошуку, включно з пошуком в ширину, за першим найкращим та методом гілок і меж. Більше того, пошук може здійснюватися послідовно, одним вузлом в кожен момент часу, або паралельно, багатьма вузлами одночасно.
ВЛВ-резолюція також є не детерміністською в тому згаданому раніше сенсі, що правило вибору визначається не правилом висновування, а окремою процедурою ухвалення рішення, що може бути чутливою до динаміки процесу виконання програми.
Простір пошуку ВЛВ-резолюції є деревом або, в якому різні гілки представляють альтернативні обчислення. У випадку програм логіки висловлень ВЛВ може бути узагальнено так, що простір пошуку стає [en], чиї вузли позначено єдиним літералами, що представляють підцілі, й вузли з'єднано або кон'юнкцією, або диз'юнкцією. В загальному випадку, коли з'єднані підцілі мають спільні змінні, представлення деревом та-або є складнішим.
Приклад
Для заданої логічної програми
q :- p
p
та мети верхнього рівня
q
простір пошуку складається з єдиної гілки, в якій q
зводиться до p
, яке зводиться до порожнього набору підцілей, сигналізуючи про успішне обчислення. В даному випадку програма є настільки простою, що для функції вибору немає ніякої ролі, і немає потреби в жодному пошуку.
В логіці тверджень ця програма представляється набором тверджень
а ціль верхнього рівня представляється цільовим твердженням з єдиним заперечним літералом
Простір пошуку складається з єдиного спростування
де представляє порожнє твердження.
Якщо до програми додається наступне твердження
q :- r
то в просторі пошуку буде додаткова гілка, чий листовий вузол r
є вузлом відмови. В Пролозі, якщо це твердження буде додано на початку оригінальної програми, то для визначення порядку, в якому досліджуватимуться гілки простору пошуку, Пролог використовуватиме порядок, в якому записано твердження. Пролог спробує цю нову гілку першою, зіткнеться з відмовою, потім повернеться до дослідження єдиної гілки оригінальної програми, і досягне успіху.
Якщо тепер до програми буде додано твердження
p :- p
то дерево пошуку міститиме нескінченну гілку. Якщо це твердження буде спробувано першим, то Пролог увійде до нескінченного циклу, й не знайде успішної гілки.
ВЛВЗВ
ВЛВЗВ (англ. SLDNF) є розширенням ВЛВ-резолюції для поводження із запереченням як відмовою (англ. negation as failure). У ВЛВЗВ цільові твердження можуть містити літерали заперечення як відмови, скажімо, у вигляді , що можуть обиратися лише тоді, коли вони не містять змінних. Коли обирається такий літерал без змінних, то піддоведення (або підобчислення) намагається визначити, чи існує ВЛВЗВ-спростування, що починається з відповідного не запереченого літералу як верхнього твердження. Вибрана підціль досягає успіху, якщо піддоведення відмовляє, і відмовляє, якщо піддоведення досягає успіху.
Див. також
Виноски
- Robert Kowalski Predicate Logic as a Programming Language [ 7 лютого 2016 у Wayback Machine.] Memo 70, Department of Artificial Intelligence, Edinburgh University. 1973. Також у Proceedings IFIP Congress, Stockholm, North Holland Publishing Co., 1974, pp. 569—574. (англ.)
- Robert Kowalski and Donald Kuehner, Linear Resolution with Selection Function [ 23 вересня 2015 у Wayback Machine.] Artificial Intelligence, Vol. 2, 1971, pp. 227-60. (англ.)
- 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 [ 3 червня 2011 у Wayback Machine.] (англ.)
Джерела
- [en], SLD-Resolution and Logic Programming [ 24 червня 2021 у Wayback Machine.] chapter 9 of Logic for Computer Science: Foundations of Automatic Theorem Proving [ 8 серпня 2018 у Wayback Machine.], онлайнова редакція 2003 року (вільна для завантаження), початково опублікована Wiley в 1986 році (англ.)
- John C. Shepherdson, SLDNF-Resolution with Equality, Journal of Automated Reasoning 8: 297—306, 1992; визначає семантики, по відношенню до яких SLDNF-резолюція з еквівалентністю є правильною та повною (англ.)
Посилання
- [1] [ 9 жовтня 2015 у Wayback Machine.] Визначення з Free On-Line Dictionary of Computing (англ.)
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
VLV rezolyu ciya vibirkova linijna rezolyuciya z viznachenimi tverdzhennyami SLD rezolyu ciya angl SLD resolution Selective Linear Definite clause resolution ce elementarne pravilo visnovuvannya sho zastosovuyetsya v logichnomu programuvanni Vono ye vdoskonalennyam rezolyuciyi sho ye yak pravilnim tak i sprostuvalno povnim dlya diz yunktiv Gorna Pravilo visnovuvannya VLVMayuchi cilove tverdzhennya L 1 L i L n displaystyle neg L 1 lor cdots lor neg L i lor cdots lor neg L n z obranim literalom L i displaystyle neg L i ta vhidne viznachene tverdzhennya L K 1 K m displaystyle L lor neg K 1 lor cdots lor neg K m chij stverdnij literal atom L displaystyle L unifikuyetsya z atomom L i displaystyle L i obranogo literalu L i displaystyle neg L i VLV rezolyuciya vivodit inshe cilove tverdzhennya v yakomu obranij literal zaminyuyetsya zaperechnimi literalami vhidnogo tverdzhennya ta zastosovuyetsya unifikuvalne pidstavlennya 8 displaystyle theta L 1 K 1 K m L n 8 displaystyle neg L 1 lor cdots lor neg K 1 lor cdots lor neg K m lor cdots lor neg L n theta V najprostishomu vipadku v logici vislovlen atomi L i displaystyle L i ta L displaystyle L ye identichnimi j unifikuvalne pidstavlennya 8 displaystyle theta ye virodzhenim Prote v zagalnishomu vipadku unifikuvalne pidstavlennya potribne shobi zrobiti ci dva literali identichnimi Pohodzhennya nazvi VLV Nazvu VLV rezolyuciya angl SLD resolution bulo dano Martenom van Emdenom angl Maarten van Emden bezimennomu pravilu visnovuvannya zaproponovanomu Robertom Kovalskim Jogo nazva pohodit vid VL rezolyuciyi angl SL resolution sho ye yak pravilnoyu tak i povnoyu dlya neobmezhenoyi tverdzhennevoyi formi logiki VLV vidpovidaye VL rezolyuciyi z viznachenimi tverdzhennyami angl SL resolution with Definite clauses Yak u VL tak i v VLV L vkazuye na toj fakt sho dovedennya rezolyuciyi mozhe buti obmezhene linijnoyu angl linear poslidovnistyu tverdzhen C 1 C 2 C l displaystyle C 1 C 2 cdots C l de verhnye tverdzhennya C 1 displaystyle C 1 ye vhidnim tverdzhennyam a kozhne inshe tverdzhennya C i 1 displaystyle C i 1 ye rezolventoyu chiyi batki ye poperednim tverdzhennyam C i displaystyle C i Dovedennya ye sprostuvannyam yaksho ostannye tverdzhennya C l displaystyle C l ye porozhnim tverdzhennyam U VLV vsi tverdzhennya v poslidovnosti ye cilovimi tverdzhennyami j inshe batkivske tverdzhennya ye vhidnim tverdzhennyam U VL rezolyuciyi inshe batkivske ye abo vhidnim tverdzhennyam abo predkovim tverdzhennyam ranishe v poslidovnosti Yak u VL tak i v VLV pershe V vkazuye na toj fakt sho yedinim literalom sho rozkladayetsya u tverdzhenni C i displaystyle C i ye toj yakij odnoznachno obrano pravilom viboru angl selection rule abo funkciyeyu viboru angl selection function U VL rezolyuciyi literal sho obirayetsya obmezheno timi sho bezposeredno pered cim bulo vvedeno do tverdzhennya V najprostishomu vipadku taku funkciyu viboru ostannim uvijshov pershim vijshov mozhe buti viznacheno poryadkom zapisu literaliv yak u Prolozi Prote u VLV rezolyuciyi funkciya viboru ye zagalnishoyu nizh u VL rezolyuciyi ta v Prolozi Tut nemaye obmezhennya na vibir literalu Obchislyuvalna interpretaciya VLV rezolyuciyiV logici tverdzhen VLV sprostuvannya pokazuye sho vhidnij nabir tverdzhen ye nezdijsnennim Prote v logichnomu programuvanni VLV sprostuvannya maye takozh i obchislyuvalnu interpretaciyu Verhnye tverdzhennya L 1 L i L n displaystyle neg L 1 lor cdots lor neg L i lor cdots lor neg L n mozhe buti interpretovano yak zaperechennya kon yunkciyi pidcilej L 1 L i L n displaystyle L 1 land cdots land L i land cdots land L n Vivedennya tverdzhennya C i 1 displaystyle C i 1 z C i displaystyle C i ye vivedennyam zasobami zvorotnogo vivodu novogo naboru pidcilej iz zastosuvannyam vhidnogo tverdzhennya yak proceduri skorochennya cilej Unifikuvalne pidstavlennya 8 displaystyle theta peredaye yak vhid z vibranoyi pidcili do tila proceduri tak i odnochasno vihid z golovi proceduri do reshti nevibranih pidcilej Porozhnye tverdzhennya ye prosto porozhnim naborom pidcilej sho signalizuye pro te sho pochatkovu kon yunkciyu pidcilej z verhnogo tverdzhennya rozv yazano Strategiyi VLV rezolyuciyiVLV rezolyuciya neyavno viznachaye derevo poshuku alternativnih obchislen v yakomu pochatkove cilove tverdzhennya pov yazuyetsya z korenem dereva Dlya kozhnogo vuzla v comu derevi ta dlya kozhnogo viznachenogo tverdzhennya v programi chiyi stverdni literali unifikuyutsya z obranim literalom u cilovomu tverdzhenni pov yazanomu z cim vuzlom isnuye dochirnij vuzol pov yazanij z cilovim tverdzhennyam otrimanim VLV rezolyuciyeyu Listovij vuzol sho ne maye dochirnih ye vuzlom uspihu yaksho pov yazane z nim cilove tverdzhennya ye porozhnim tverdzhennyam Vin ye vuzlom vidmovi yaksho pov yazane z nim cilove tverdzhennya ye neporozhnim ale jogo obranij literal ne unifikuyetsya zi stverdnim literalom zhodnogo vhidnogo tverdzhennya VLV rezolyuciya ye ne deterministskoyu v tomu sensi sho vona ne viznachaye strategiyu poshuku dlya doslidzhennya dereva poshuku Prolog shukaye derevom v glibinu po odnij gilci v kozhen moment chasu zastosovuyuchi vertannya koli stikayetsya z vuzlom vidmovi Poshuk v glibinu ye duzhe efektivnim v jogo spozhivanni obchislyuvalnih resursiv ale vin ye nepovnim yaksho prostir poshuku mistit neskinchenni gilki j strategiya poshuku viddaye perevagu poshuku nimi pered skinchennimi gilkami obchislyuvannya ne zavershuyetsya Mozhlivimi ye takozh j inshi strategiyi poshuku vklyuchno z poshukom v shirinu za pershim najkrashim ta metodom gilok i mezh Bilshe togo poshuk mozhe zdijsnyuvatisya poslidovno odnim vuzlom v kozhen moment chasu abo paralelno bagatma vuzlami odnochasno VLV rezolyuciya takozh ye ne deterministskoyu v tomu zgadanomu ranishe sensi sho pravilo viboru viznachayetsya ne pravilom visnovuvannya a okremoyu proceduroyu uhvalennya rishennya sho mozhe buti chutlivoyu do dinamiki procesu vikonannya programi Prostir poshuku VLV rezolyuciyi ye derevom abo v yakomu rizni gilki predstavlyayut alternativni obchislennya U vipadku program logiki vislovlen VLV mozhe buti uzagalneno tak sho prostir poshuku staye en chiyi vuzli poznacheno yedinim literalami sho predstavlyayut pidcili j vuzli z yednano abo kon yunkciyeyu abo diz yunkciyeyu V zagalnomu vipadku koli z yednani pidcili mayut spilni zminni predstavlennya derevom ta abo ye skladnishim PrikladDlya zadanoyi logichnoyi programi q p p ta meti verhnogo rivnya q prostir poshuku skladayetsya z yedinoyi gilki v yakij q zvoditsya do p yake zvoditsya do porozhnogo naboru pidcilej signalizuyuchi pro uspishne obchislennya V danomu vipadku programa ye nastilki prostoyu sho dlya funkciyi viboru nemaye niyakoyi roli i nemaye potrebi v zhodnomu poshuku V logici tverdzhen cya programa predstavlyayetsya naborom tverdzhen q p displaystyle q lor neg p p displaystyle p a cil verhnogo rivnya predstavlyayetsya cilovim tverdzhennyam z yedinim zaperechnim literalom q displaystyle neg q Prostir poshuku skladayetsya z yedinogo sprostuvannya q p f a l s e displaystyle neg q neg p mathit false de f a l s e displaystyle mathit false predstavlyaye porozhnye tverdzhennya Yaksho do programi dodayetsya nastupne tverdzhennya q r to v prostori poshuku bude dodatkova gilka chij listovij vuzol r ye vuzlom vidmovi V Prolozi yaksho ce tverdzhennya bude dodano na pochatku originalnoyi programi to dlya viznachennya poryadku v yakomu doslidzhuvatimutsya gilki prostoru poshuku Prolog vikoristovuvatime poryadok v yakomu zapisano tverdzhennya Prolog sprobuye cyu novu gilku pershoyu zitknetsya z vidmovoyu potim povernetsya do doslidzhennya yedinoyi gilki originalnoyi programi i dosyagne uspihu Yaksho teper do programi bude dodano tverdzhennya p p to derevo poshuku mistitime neskinchennu gilku Yaksho ce tverdzhennya bude sprobuvano pershim to Prolog uvijde do neskinchennogo ciklu j ne znajde uspishnoyi gilki VLVZVVLVZV angl SLDNF ye rozshirennyam VLV rezolyuciyi dlya povodzhennya iz zaperechennyam yak vidmovoyu angl negation as failure U VLVZV cilovi tverdzhennya mozhut mistiti literali zaperechennya yak vidmovi skazhimo u viglyadi n o t p displaystyle not p sho mozhut obiratisya lishe todi koli voni ne mistyat zminnih Koli obirayetsya takij literal bez zminnih to piddovedennya abo pidobchislennya namagayetsya viznachiti chi isnuye VLVZV sprostuvannya sho pochinayetsya z vidpovidnogo ne zaperechenogo literalu p displaystyle p yak verhnogo tverdzhennya Vibrana pidcil n o t p displaystyle not p dosyagaye uspihu yaksho piddovedennya vidmovlyaye i vidmovlyaye yaksho piddovedennya dosyagaye uspihu Div takozhDzhon Alan RobinsonVinoskiRobert Kowalski Predicate Logic as a Programming Language 7 lyutogo 2016 u Wayback Machine Memo 70 Department of Artificial Intelligence Edinburgh University 1973 Takozh u Proceedings IFIP Congress Stockholm North Holland Publishing Co 1974 pp 569 574 angl Robert Kowalski and Donald Kuehner Linear Resolution with Selection Function 23 veresnya 2015 u Wayback Machine Artificial Intelligence Vol 2 1971 pp 227 60 angl 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 3 chervnya 2011 u Wayback Machine angl Dzherela en SLD Resolution and Logic Programming 24 chervnya 2021 u Wayback Machine chapter 9 of Logic for Computer Science Foundations of Automatic Theorem Proving 8 serpnya 2018 u Wayback Machine onlajnova redakciya 2003 roku vilna dlya zavantazhennya pochatkovo opublikovana Wiley v 1986 roci angl John C Shepherdson SLDNF Resolution with Equality Journal of Automated Reasoning 8 297 306 1992 viznachaye semantiki po vidnoshennyu do yakih SLDNF rezolyuciya z ekvivalentnistyu ye pravilnoyu ta povnoyu angl Posilannya 1 9 zhovtnya 2015 u Wayback Machine Viznachennya z Free On Line Dictionary of Computing angl