www.wikidata.uk-ua.nina.az

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

Правило резолюцій

Правило резолюцій — це правило висновування, що сходить до методу доказу теорем через пошук протиріч; використовується в логіці висловлювань і логіці предикатів першого порядку. Правило резолюцій, що застосовується послідовно для списку резольвент, дозволяє відповісти на питання, чи існує у вхідній множині логічих виразів протиріччя. Правило резолюцій запропоновано в 1930 році в докторській дисертації Жака Ербрана для доведення теорем у формальних системах першого порядку. Правило розроблено Джоном Аланом Робінсоном в 1965 році.

Алгоритми доказу виводимості , побудовані на основі цього методу, застосовуються в багатьох системах штучного інтелекту, а також є фундаментом, на якому побудовано мову логічного програмування «Пролог».

Логіка висловлень Редагувати

Правило резолюцій першочергово застосовується до диз'юнктів  — диз'юнкцій пропозиційних змінних чи їх заперечень. Правило застосовується до двох диз'юнктів у випадку, коли вони містять пропозиційні змінні, одна з яких є запереченням другої. Наприклад:

де є доповненням , (наприклад , а )

Для можливості використання цього правила необхідно записати формулу у кон'юнктивній нормальній формулі. Довільна формула логіки висловлень еквівалентна деякій формулі цього виду. При записі формули у кон'юнктивній формі кожен диз'юнкт можна подати як множину літералів (пропозиційних формул чи їх заперечень), а саму формулу як множину диз'юнктів. Наприклад формулу:

можна подати так:

Також таким чином можна визначити правило резолюцій:

Позначимо:

Деяка формула записана у КНФ є невиконуваною тоді і тільки тоді, коли . Як наслідок з цього для довільних формул формула є логічним наслідком тих формул тоді і тільки тоді, коли . Тобто система формального виводу заснована на правилі резолюцій є коректною і повною.

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

Нехай є формули:

Потрібно довести що:

Спершу приведімо дані формули до кон'юнктивної нормальної форми:

Далі запишемо:

Послідовно використовуючи правило резолюцій отримуємо:

що й доводить твердження.

Числення висловлювань Редагувати

Нехай і  — дві пропозиції в численні висловлювань, і нехай , а , де  — пропозіціональная змінна, а й  — будь-які пропозиції (зокрема, може бути, порожні або складаються тільки з одного літерала).

Правило виводу

називається правилом резолюцій.

Пропозиції C1 і C2 називаються резольвуючими (або батьківськими), пропозиція   — резольвентою, а формули і  — контрарними літералами. Загалом в правилі резолюції беруться два вирази і виробляється новий вираз, що містить всі літерали двох початкових виразів, за винятком двох взаємно обернених літералів.

Метод резолюції Редагувати

Метод резолюцій запропонований у 1930 р. в докторській дисертації Жака Ербрана для доведення теорем у формальних системах першого порядку. Метод резолюцій спирається на обчислення резольвент. Існує теорема, яка стверджує, що питання про доказовість довільної формули в численні предикатів зводиться до питання про вивідність порожнього списку в обчисленні резольвент. Тому доведення того, що список формул в обчисленні резольвент порожній, еквівалентне доведенню хибності формули в численні предикатів.

Рішення в логічній моделі на основі методу резолюцій Дано твердження: «Сократ — людина»;

«Людина — це жива істота»;

«Всі живі істоти смертні».

Потрібно методом резолюцій довести твердження «Сократ смертний».

Рішення: Крок 1. Перетворимо висловлювання на диз'юнктивну форму;

Крок 2. Запишемо заперечення цільового виразу (необхідного виводу), тобто «Сократ безсмертний»;

Крок 3. Скласти кон'юнкцію всіх диз'юнктів, включивши в неї заперечення цільового виразу;

Крок 4. У циклі проведемо операцію пошуку резольвентів над кожною парою диз'юнктів;

Отримання порожнього диз'юнкта означає, що висловлювання «Сократ безсмертний» — хибне, значить, істинне висловлювання «Сократ смертний».

Доказ теорем зводиться до доказу того, що деяка формула (гіпотеза теореми) є логічним наслідком множини формул (припущень). Тобто сама теорема може бути сформульована таким чином: «якщо істинні, то істинна й ».

Для доказу того, що формула є логічним наслідком множини формул , метод резолюцій застосовується наступним чином. Спочатку складається множина формул . Потім кожна з цих формул приводиться до КНФ (сполучення диз'юнктів) і в отриманих формулах закреслюються знаки кон'юнкції. Виходить безліч диз'юнктів . І, нарешті, шукається висновок порожнього диз'юнктів з . Якщо порожній диз'юнкт виводимо з , то формула є логічним наслідком формул . Якщо з не можна вивести #, то не є логічним наслідком формул . Такий метод доведення теорем називається методом резолюцій .
Розглянемо приклад докази методом резолюцій. Нехай у нас є наступні твердження:

Доведемо твердження «яблуко смачне». Введемо множину формул, що описують прості висловлювання, відповідні вищенаведеним твердженням. Нехай

Тоді самі твердження можна записати у вигляді складних формул:

Тоді твердження, яке треба довести, виражається формулою X3.
Отже, доведемо, що X3 є логічним наслідком та . Спочатку складаємо множину формул з запереченням доказуваного висловлювання; отримуємо:

Тепер приводимо всі формули до кон'юнктівной нормальній форми і закреслюємо кон'юнкції. Отримуємо наступну множину диз'юнктів:

Далі шукаємо висновок порожнього диз'юнкта.
Застосовуємо до першого і третього диз'юнкта правило резолюції:

Застосовуємо до четвертого і п'ятого диз'юнкт правило резолюції:

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

Логіка першого порядку Редагувати

Для двох літералів логіки першого порядку існує уніфікація, якщо існує така заміна їх символів змінних деякими термами, що дані літерали стають ідентичними. Наприклад: для і , існує уніфікація, що визначається заміною . Натомість для і уніфікація неможлива.

Нехай тепер два диз'юнкти, що мають два предикати один з яких із запереченням, а другий ні і для яких існує уніфікація. Тоді резольвента двох диз'юнктів визначається:

Нехай тепер  — формула записана у нормальній формі Сколема. Незважаючи на квантори загальності цю формулу можна подати як об'єднання диз'юнктів.

Позначимо:

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

Деяка формула записана у нормальній формі Сколема є невиконуваною тоді і тільки тоді коли . З властивостей сколемізації відомо, що для довільної формули логіки першого порядку існує формула у нормальній формі Сколема, що виконується тоді і тільки тоді коли виконується початкова формула. Як наслідок з цього для довільних формул формула є логічним наслідком тих формул тоді і тільки тоді, коли . Тобто система формального виводу заснована на правилі резолюцій є коректною і повною і в цьому випадку.

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

Доведемо, що формула є логічно загальнозначимою: Спершу слід використати процедуру сколемізації:

Відкидаючи квантор загальності:

Далі послідовно використовується правило резолюцій:

заміна (x → a)

заміна (x → a)

що й доводить твердження.

Обчислення предикатів Редагувати

Нехай C1 та C2 — дві пропозиції в численні предикатів.

Правило виводу

називається правилом резолюції в численні предикатів, якщо в пропозиціях C1 та C2 існують уніфіцировані контрарні літерали P1 та P2, тобто , а , причому атомарні формули P1 и P2 є уніфікуючим найбільш загальним уніфікатором ..

У цьому випадку резольвенти пропозицій C1 та C2 є пропозиція C1 и C2, отримане з пропозиції застосуванням уніфікатора .

Однак внаслідок нерозв'зності логіки предикатів першого порядку для здійсненної (несуперечливої) множини диз'юнктів процедура, заснована на принципі резолюції, може працювати нескінченно довго. Зазвичай резолюція застосовується в логічному програмуванні в сукупності з прямим або зворотнім методом міркування. Прямий метод (від посилок) з посилок А, В виводить висновок В (правило modus ponens). Основний недолік прямого методу міркування полягає в його ненаправленості: повторні застосування методу зазвичай призводять до різкого зростання проміжних висновків, не пов'язаних з цільовим ув'язненням.
Зворотний метод (від мети) є спрямованим: з бажаного висновку В тих самих посилок він виводить новий подціловий висновок А. Кожен крок висновування в цьому випадку завжди пов'язаний з спочатку поставленою метою.

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

Висновок в логічних моделях Редагувати

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

Найбільш часто використовуються два методи. Перший — метод правил виводу або метод природного (натурального) висновування, названий так тому, що використовуваний тип міркувань в численні предикатів наближається до звичайного людського розуміння. Другий — метод резолюцій. У його основі лежить літочислення резольвент.

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

  1. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем стр. 77
  2. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем стр. 85

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

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

  1. J. Alan Robinson (1965), A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM (JACM), Volume 12, Issue 1, pp. 23-41.
  2. Leitsch, Alexander (1997). The Resolution Calculus. Springer-Verlag.
  3. Gallier, Jean H. (1986). Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row Publishers.
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри
Дата публікації:
Pravilo rezolyucij ce pravilo visnovuvannya sho shodit do metodu dokazu teorem cherez poshuk protirich vikoristovuyetsya v logici vislovlyuvan i logici predikativ pershogo poryadku Pravilo rezolyucij sho zastosovuyetsya poslidovno dlya spisku rezolvent dozvolyaye vidpovisti na pitannya chi isnuye u vhidnij mnozhini logichih viraziv protirichchya Pravilo rezolyucij zaproponovano v 1930 roci v doktorskij disertaciyi Zhaka Erbrana dlya dovedennya teorem u formalnih sistemah pershogo poryadku Pravilo rozrobleno Dzhonom Alanom Robinsonom v 1965 roci Algoritmi dokazu vivodimosti A B displaystyle A vdash B pobudovani na osnovi cogo metodu zastosovuyutsya v bagatoh sistemah shtuchnogo intelektu a takozh ye fundamentom na yakomu pobudovano movu logichnogo programuvannya Prolog Zmist 1 Logika vislovlen 1 1 Priklad 2 Chislennya vislovlyuvan 2 1 Metod rezolyuciyi 3 Logika pershogo poryadku 3 1 Priklad 4 Obchislennya predikativ 5 Visnovok v logichnih modelyah 6 Primitki 7 Div takozh 8 DzherelaLogika vislovlen RedaguvatiPravilo rezolyucij pershochergovo zastosovuyetsya do diz yunktiv diz yunkcij propozicijnih zminnih chi yih zaperechen Pravilo zastosovuyetsya do dvoh diz yunktiv u vipadku koli voni mistyat propozicijni zminni odna z yakih ye zaperechennyam drugoyi Napriklad a 1 a i a n b 1 b j b m a 1 a i 1 a i 1 a n b 1 b j 1 b j 1 b m displaystyle frac a 1 lor ldots vee a i vee ldots lor a n quad b 1 lor ldots vee b j vee ldots lor b m a 1 lor ldots lor a i 1 lor a i 1 lor ldots lor a n lor b 1 lor ldots lor b j 1 lor b j 1 lor ldots lor b m nbsp de a i displaystyle a i nbsp ye dopovnennyam b j displaystyle b j nbsp napriklad a i x displaystyle a i x nbsp a b i x displaystyle b i lnot x nbsp Dlya mozhlivosti vikoristannya cogo pravila neobhidno zapisati formulu u kon yunktivnij normalnij formuli Dovilna formula logiki vislovlen ekvivalentna deyakij formuli cogo vidu Pri zapisi formuli u kon yunktivnij formi kozhen diz yunkt mozhna podati yak mnozhinu literaliv propozicijnih formul chi yih zaperechen a samu formulu yak mnozhinu diz yunktiv Napriklad formulu p q r q r s p s q s displaystyle neg p wedge q vee r vee q wedge neg r vee neg s wedge p vee s wedge neg q vee neg s nbsp mozhna podati tak p q r r s p s q s displaystyle neg p q r neg r neg s p s neg q neg s nbsp Takozh takim chinom mozhna viznachiti pravilo rezolyucij C p C p C C displaystyle frac C p quad C neg p C C nbsp Poznachimo R e s F F R displaystyle Res F F cup R nbsp de R displaystyle R nbsp diz yunkt oderzhanij za pravilom rezolyucij z deyakih diz yunktiv formuli F displaystyle F nbsp i Mit R e s F n N R e s n F displaystyle Res star F bigcup n in mathbb N Res n F nbsp ob yednannya vsih diz yunktiv oderzhanih z diz yunktiv formuli F displaystyle F nbsp za skinchennu kilkist vikoristan pravila rezolyucij Deyaka formula F displaystyle F nbsp zapisana u KNF ye nevikonuvanoyu todi i tilki todi koli R e s F displaystyle emptyset in Res star F nbsp Yak naslidok z cogo dlya dovilnih formul A 1 A 2 A n displaystyle A 1 A 2 ldots A n nbsp formula F displaystyle F nbsp ye logichnim naslidkom tih formul todi i tilki todi koli R e s A 1 A 2 A n F displaystyle emptyset in Res star A 1 lor A 2 lor ldots lor A n lor lnot F nbsp Tobto sistema formalnogo vivodu zasnovana na pravili rezolyucij ye korektnoyu i povnoyu Priklad Redaguvati Nehaj ye formuli P S displaystyle P rightarrow S nbsp S P displaystyle S rightarrow neg P nbsp S P displaystyle neg S rightarrow P nbsp Potribno dovesti sho P S S P S P S displaystyle P rightarrow S S rightarrow neg P neg S rightarrow P models S nbsp Spershu privedimo dani formuli do kon yunktivnoyi normalnoyi formi P S P S displaystyle P rightarrow S quad equiv quad neg P vee S nbsp S P S P displaystyle S rightarrow neg P quad equiv quad neg S vee neg P nbsp S P S P displaystyle neg S rightarrow P quad equiv quad S vee P nbsp Dali zapishemo P S S P S P S displaystyle neg P S neg S neg P S P neg S nbsp Poslidovno vikoristovuyuchi pravilo rezolyucij otrimuyemo S S P P displaystyle frac neg S qquad S P P nbsp S P S P displaystyle frac neg S qquad neg P S neg P nbsp P P displaystyle frac P qquad neg P emptyset nbsp sho j dovodit tverdzhennya Chislennya vislovlyuvan RedaguvatiNehaj C 1 displaystyle C 1 nbsp i C 2 displaystyle C 2 nbsp dvi propoziciyi v chislenni vislovlyuvan i nehaj C 1 P C 1 displaystyle C 1 P lor C 1 nbsp a C 2 P C 2 displaystyle C 2 lnot P lor C 2 nbsp de P displaystyle P nbsp propozicionalnaya zminna a C 1 displaystyle C 1 nbsp j C 2 displaystyle C 2 nbsp bud yaki propoziciyi zokrema mozhe buti porozhni abo skladayutsya tilki z odnogo literala Pravilo vivoduC 1 C 2 C 1 C 2 displaystyle frac C 1 C 2 C 1 lor C 2 nbsp nazivayetsya pravilom rezolyucij 1 Propoziciyi C1 i C2 nazivayutsya rezolvuyuchimi abo batkivskimi propoziciya C 1 C 2 displaystyle C 1 lor C 2 nbsp rezolventoyu a formuli P displaystyle P nbsp i P displaystyle lnot P nbsp kontrarnimi literalami Zagalom v pravili rezolyuciyi berutsya dva virazi i viroblyayetsya novij viraz sho mistit vsi literali dvoh pochatkovih viraziv za vinyatkom dvoh vzayemno obernenih literaliv Metod rezolyuciyi Redaguvati Metod rezolyucij zaproponovanij u 1930 r v doktorskij disertaciyi Zhaka Erbrana dlya dovedennya teorem u formalnih sistemah pershogo poryadku Metod rezolyucij spirayetsya na obchislennya rezolvent Isnuye teorema yaka stverdzhuye sho pitannya pro dokazovist dovilnoyi formuli v chislenni predikativ zvoditsya do pitannya pro vividnist porozhnogo spisku v obchislenni rezolvent Tomu dovedennya togo sho spisok formul v obchislenni rezolvent porozhnij ekvivalentne dovedennyu hibnosti formuli v chislenni predikativ Rishennya v logichnij modeli na osnovi metodu rezolyucij Dano tverdzhennya Sokrat lyudina Lyudina ce zhiva istota Vsi zhivi istoti smertni Potribno metodom rezolyucij dovesti tverdzhennya Sokrat smertnij Rishennya Krok 1 Peretvorimo vislovlyuvannya na diz yunktivnu formu Krok 2 Zapishemo zaperechennya cilovogo virazu neobhidnogo vivodu tobto Sokrat bezsmertnij Krok 3 Sklasti kon yunkciyu vsih diz yunktiv vklyuchivshi v neyi zaperechennya cilovogo virazu Krok 4 U cikli provedemo operaciyu poshuku rezolventiv nad kozhnoyu paroyu diz yunktiv Otrimannya porozhnogo diz yunkta oznachaye sho vislovlyuvannya Sokrat bezsmertnij hibne znachit istinne vislovlyuvannya Sokrat smertnij Dokaz teorem zvoditsya do dokazu togo sho deyaka formula G displaystyle G nbsp gipoteza teoremi ye logichnim naslidkom mnozhini formul F 1 F k displaystyle F 1 F k nbsp pripushen Tobto sama teorema mozhe buti sformulovana takim chinom yaksho F 1 F k displaystyle F 1 F k nbsp istinni to istinna j G displaystyle G nbsp Dlya dokazu togo sho formula G displaystyle G nbsp ye logichnim naslidkom mnozhini formul F 1 F k displaystyle F 1 F k nbsp metod rezolyucij zastosovuyetsya nastupnim chinom Spochatku skladayetsya mnozhina formul f F 1 F k G g displaystyle mathcal f F 1 F k neg G mathcal g nbsp Potim kozhna z cih formul privoditsya do KNF spoluchennya diz yunktiv i v otrimanih formulah zakreslyuyutsya znaki kon yunkciyi Vihodit bezlich diz yunktiv S displaystyle S nbsp I nareshti shukayetsya visnovok porozhnogo diz yunktiv z S displaystyle S nbsp Yaksho porozhnij diz yunkt vivodimo z S displaystyle S nbsp to formula G displaystyle G nbsp ye logichnim naslidkom formul F 1 F k displaystyle F 1 F k nbsp Yaksho z S displaystyle S nbsp ne mozhna vivesti to G displaystyle G nbsp ne ye logichnim naslidkom formul F 1 F k displaystyle F 1 F k nbsp Takij metod dovedennya teorem nazivayetsya metodom rezolyucij Rozglyanemo priklad dokazi metodom rezolyucij Nehaj u nas ye nastupni tverdzhennya Yabluko chervone i aromatne Yaksho yabluko chervone to yabluko smachne Dovedemo tverdzhennya yabluko smachne Vvedemo mnozhinu formul sho opisuyut prosti vislovlyuvannya vidpovidni vishenavedenim tverdzhennyam Nehaj X1 Yabluko chervone X2 Yabluko aromatne X3 Yabluko smachne Todi sami tverdzhennya mozhna zapisati u viglyadi skladnih formul X 1 amp X 2 displaystyle X1 And X2 nbsp Yabluko chervone i aromatne X 1 X 3 displaystyle X1 rightarrow X3 nbsp Yaksho yabluko chervone to yabluko smachne Todi tverdzhennya yake treba dovesti virazhayetsya formuloyu X3 Otzhe dovedemo sho X3 ye logichnim naslidkom X 1 amp X 2 displaystyle X1 And X2 nbsp ta X 1 X 3 displaystyle X1 rightarrow X3 nbsp Spochatku skladayemo mnozhinu formul z zaperechennyam dokazuvanogo vislovlyuvannya otrimuyemo f X 1 amp X 2 X 1 X 3 X 3 g displaystyle mathcal f X1 And X2 X1 rightarrow X3 neg X3 mathcal g nbsp Teper privodimo vsi formuli do kon yunktivnoj normalnij formi i zakreslyuyemo kon yunkciyi Otrimuyemo nastupnu mnozhinu diz yunktiv f X 1 X 2 X 1 X 3 X 3 g displaystyle mathcal f X1 X2 neg X1 vee X3 neg X3 mathcal g nbsp Dali shukayemo visnovok porozhnogo diz yunkta Zastosovuyemo do pershogo i tretogo diz yunkta pravilo rezolyuciyi f X 1 X 2 X 1 X 3 X 3 X 3 g displaystyle mathcal f X1 X2 neg X1 vee X3 neg X3 X3 mathcal g nbsp Zastosovuyemo do chetvertogo i p yatogo diz yunkt pravilo rezolyuciyi f X 1 X 2 X 1 X 3 X 3 X 3 g displaystyle mathcal f X1 X2 neg X1 vee X3 neg X3 X3 mathcal g nbsp Takim chinom porozhnij diz yunkt vivedenij otzhe viraz iz zaperechennyam vislovlyuvannya sprostovano otzhe same vislovlyuvannya dovedeno V cilomu metod rezolyucij cikavij zavdyaki prostoti ta sistemnosti ale zastosuyemo tilki dlya obmezhenogo chisla vipadkiv dovedennya ne povinno mati veliku glibinu a chislo potencijnih rezolyucij ne povinno buti velikim Krim metodu rezolyucij i pravil vivodu isnuyut inshi metodi otrimannya visnovkiv u logici predikativ Logika pershogo poryadku RedaguvatiDlya dvoh literaliv logiki pershogo poryadku isnuye unifikaciya yaksho isnuye taka zamina yih simvoliv zminnih deyakimi termami sho dani literali stayut identichnimi Napriklad dlya P x a y displaystyle P x a y nbsp i P c a z displaystyle P c a z nbsp isnuye unifikaciya sho viznachayetsya zaminoyu x c y z displaystyle x to c y to z nbsp Natomist dlya P x a y displaystyle P x a y nbsp i P c b z displaystyle P c b z nbsp unifikaciya nemozhliva Nehaj teper C 1 C 2 displaystyle C 1 C 2 nbsp dva diz yunkti sho mayut dva predikati odin z yakih iz zaperechennyam a drugij ni i dlya yakih isnuye unifikaciya Todi rezolventa dvoh diz yunktiv viznachayetsya C R C 1 C 2 L 1 L 2 displaystyle C R C 1 cup C 2 setminus L 1 neg L 2 nbsp Nehaj teper F displaystyle F nbsp formula zapisana u normalnij formi Skolema Nezvazhayuchi na kvantori zagalnosti cyu formulu mozhna podati yak ob yednannya diz yunktiv Poznachimo R e s F F R displaystyle Res F F cup R nbsp de R displaystyle R nbsp diz yunkt oderzhanij za pravilom rezolyucij z deyakih diz yunktiv formuli F displaystyle F nbsp iR e s F n N R e s n F displaystyle Res star F bigcup n in mathbb N Res n F nbsp ob yednannya vsih diz yunktiv oderzhanih z diz yunktiv formuli F displaystyle F nbsp za skinchennu kilkist vikoristan pravila rezolyucij Deyaka formula F displaystyle F nbsp zapisana u normalnij formi Skolema ye nevikonuvanoyu todi i tilki todi koli R e s F displaystyle emptyset in Res star F nbsp Z vlastivostej skolemizaciyi vidomo sho dlya dovilnoyi formuli logiki pershogo poryadku isnuye formula u normalnij formi Skolema sho vikonuyetsya todi i tilki todi koli vikonuyetsya pochatkova formula Yak naslidok z cogo dlya dovilnih formul A 1 A 2 A n displaystyle A 1 A 2 ldots A n nbsp formula F displaystyle F nbsp ye logichnim naslidkom tih formul todi i tilki todi koli R e s A 1 A 2 A n F displaystyle emptyset in Res star A 1 lor A 2 lor ldots lor A n lor lnot F nbsp Tobto sistema formalnogo vivodu zasnovana na pravili rezolyucij ye korektnoyu i povnoyu i v comu vipadku Priklad Redaguvati Dovedemo sho formula ye logichno zagalnoznachimoyu x p x q x p a q a displaystyle forall x p x vee q x wedge neg p a rightarrow q a nbsp Spershu slid vikoristati proceduru skolemizaciyi x p x q x p a q a displaystyle neg forall x p x vee q x wedge neg p a rightarrow q a nbsp x p x q x p a q a displaystyle equiv neg neg forall x p x vee q x wedge neg p a vee q a nbsp x p x q x p a q a displaystyle equiv forall x p x vee q x wedge neg p a vee q a nbsp x p x q x p a q a displaystyle equiv forall x p x vee q x wedge neg p a wedge neg q a nbsp Vidkidayuchi kvantor zagalnosti p x q x p a q a displaystyle p x vee q x wedge neg p a wedge neg q a nbsp p x q x p a q a displaystyle p x q x neg p a neg q a nbsp Dali poslidovno vikoristovuyetsya pravilo rezolyucij p x q x p a q a displaystyle frac p x q x quad neg p a q a nbsp zamina x a q a q a displaystyle frac neg q a quad q a emptyset nbsp zamina x a sho j dovodit tverdzhennya Obchislennya predikativ RedaguvatiNehaj C1 ta C2 dvi propoziciyi v chislenni predikativ Pravilo vivodu C 1 C 2 C 1 C 2 s R displaystyle frac C 1 C 2 C 1 lor C 2 sigma R nbsp nazivayetsya pravilom rezolyuciyi v chislenni predikativ yaksho v propoziciyah C1 ta C2 isnuyut unificirovani kontrarni literali P1 ta P2 tobto C 1 P 1 C 1 displaystyle C 1 P 1 lor C 1 nbsp a C 2 P 2 C 2 displaystyle C 2 lnot P 2 lor C 2 nbsp prichomu atomarni formuli P1 i P2 ye unifikuyuchim najbilsh zagalnim unifikatorom s displaystyle sigma nbsp U comu vipadku rezolventi propozicij C1 ta C2 ye propoziciya C1 i C2 otrimane z propoziciyi C 1 C 2 displaystyle C 1 lor C 2 nbsp zastosuvannyam unifikatora s displaystyle sigma nbsp 2 Odnak vnaslidok nerozv znosti logiki predikativ pershogo poryadku dlya zdijsnennoyi nesuperechlivoyi mnozhini diz yunktiv procedura zasnovana na principi rezolyuciyi mozhe pracyuvati neskinchenno dovgo Zazvichaj rezolyuciya zastosovuyetsya v logichnomu programuvanni v sukupnosti z pryamim abo zvorotnim metodom mirkuvannya Pryamij metod vid posilok z posilok A V vivodit visnovok V pravilo modus ponens Osnovnij nedolik pryamogo metodu mirkuvannya polyagaye v jogo nenapravlenosti povtorni zastosuvannya metodu zazvichaj prizvodyat do rizkogo zrostannya promizhnih visnovkiv ne pov yazanih z cilovim uv yaznennyam Zvorotnij metod vid meti ye spryamovanim z bazhanogo visnovku V tih samih posilok vin vivodit novij podcilovij visnovok A Kozhen krok visnovuvannya v comu vipadku zavzhdi pov yazanij z spochatku postavlenoyu metoyu Istotnij nedolik principu rezolyuciyi polyagaye u formuvanni na kozhnomu kroci vivodu bezlichi rezolventiv novih diz yunktiv bilshist z yakih viyavlyayutsya zajvimi U zv yazku z cim rozrobleni rizni modifikaciyi principu rezolyuciyi sho vikoristovuyut bilsh efektivni strategiyi poshuku i riznogo rodu obmezhennya na vid vihidnih diz yunktiv Visnovok v logichnih modelyah RedaguvatiVisnovok u formalnij logichnij sistemi ye proceduroyu yaka iz zadanoyi grupi viraziv vivodit vidminne vid zadanih semantichno pravilnij viraz Cya procedura predstavlena u pevnij formi i ye pravilom vivodu Yaksho grupa viraziv sho utvoryuye posilku ye istinnoyu to povinno garantuvatisya sho zastosuvannya pravila visnovuvannya zabezpechit otrimannya istinnogo virazu yak visnovku Najbilsh chasto vikoristovuyutsya dva metodi Pershij metod pravil vivodu abo metod prirodnogo naturalnogo visnovuvannya nazvanij tak tomu sho vikoristovuvanij tip mirkuvan v chislenni predikativ nablizhayetsya do zvichajnogo lyudskogo rozuminnya Drugij metod rezolyucij U jogo osnovi lezhit litochislennya rezolvent Primitki Redaguvati Chen Ch Li R Matematicheskaya logika i avtomaticheskoe dokazatelstvo teorem str 77 Chen Ch Li R Matematicheskaya logika i avtomaticheskoe dokazatelstvo teorem str 85Div takozh RedaguvatiChislennya vislovlen Logika pershogo poryadku Kon yunktivna normalna forma Normalna forma Skolema Detalnij opis metodu rezolyucijDzherela RedaguvatiJ Alan Robinson 1965 A Machine Oriented Logic Based on the Resolution Principle Journal of the ACM JACM Volume 12 Issue 1 pp 23 41 Leitsch Alexander 1997 The Resolution Calculus Springer Verlag Gallier Jean H 1986 Logic for Computer Science Foundations of Automatic Theorem Proving Harper amp Row Publishers Otrimano z https uk wikipedia org w index php title Pravilo rezolyucij amp oldid 37718153