Спец часть (часть 1) (3 поток) (2015) (by Кибитова) (1161601), страница 13
Текст из файла (страница 13)
Правило резолюцииПравило резолюцииЕЗОЛЮТИВНЫЙ ВЫВОДРЕЗОЛЮТИВНЫЙВЫВОД00D1 _ L1 , D2 _ ¬L0 20НОУ(L , L ),✓2D_L,D_¬L2 1 212(D10 _ D20 )✓ 1, ✓ 2 НОУ(L1 , L2 )00 (D1 _ D2 )✓Правило склейки.Правило склейки.Пусть D1 = D10 _ L1 _ L2 � дизъюнкт.Пусть D1 = D10 _ L1 _ L2 � дизъюнкт.Пусть ⌘ 2 НОУ(L1 , L2 ).Пусть ⌘ 2 НОУ(L1 , L2 ).Тогда дизъюнкт D0 = (D10 _ L1 )⌘ называетсясклейкой0 _ L )⌘ называется склейкойТогдадизъюнктD=(D011дизъюнкта D1 .дизъюнкта D1 .Пара литер L1 и L2 называется склеиваемой парой .Пара литер L1 и L2 называется склеиваемой парой .Правило склейкиПравило склейкиD10 _ L1 _ L20 НОУ(L , L ), ⌘D221 _ L1 _ L12ВЫВОДРЕЗОЛЮТИВНЫЙ(D10 _ L1 )⌘, ⌘ 2 НОУ(L1 , L2 )0(D1 _ L1 )⌘ Определение резолютивного вывода.Пусть S = {D1 , D2 , .
. . , DN } � система дизъюнктов.Резолютивным выводом из системы дизъюнктов S называетсяконечная последовательность дизъюнктов0D10 , D20 , . . . , Di0 , Di+1, . . . , Dn0 ,в которой для любого i, 1 i n, выполняется одно из трехусловий:1. либо Di0 � вариант некоторого дизъюнкта из S;2. либо Di0 � резольвента дизъюнктов Dj0 и Dk0 , где j, k < i;3. либо D 0 � склейка дизъюнкта D 0 , где j < i.ijРЕЗОЛЮТИВНЫЙВЫВОД000Дизъюнкты D1 , D2 , . . . , Dn считаются резолютивновыводимыми из системы S.
Резолютивный вывод называется успешным (или, по другому,резолютивным опровержением ), если этот вывод оканчиваетсяпустым дизъюнктом ⇤.Успешный вывод � это свидетельство того, что системадизъюнктов S противоречива и опровергнуто предположениео ее выполнимости!Теорема корректности резолютивного выводаЕсли из системы дизъюнктов S резолютивно выводим пустойдизъюнкт ⇤, то S � противоречивая система дизъюнктов.Теорема о полноте резолютивного выводаЕсли S � противоречивая система дизъюнктов, то из S пустымпустымдизъюнктомдизъюнктом⇤.⇤.УспешныйУспешныйвыводвывод��этоэтосвидетельствосвидетельствотого,того,чточтосистемасистемадизъюнктовдизъюнктовSSпротиворечивапротиворечиваииопровергнутоопровергнутопредположениепредположениеооеееевыполнимости!выполнимости!ТеоремаТеоремакорректностикорректностирезолютивногорезолютивноговыводавыводаЕслиЕслиизизсистемысистемыдизъюнктовдизъюнктовSSрезолютивнорезолютивновыводимвыводимпустойпустойдизъюнкт⇤,тоS�противоречиваясистемадизъюнктов.дизъюнкт ⇤, то S � противоречивая система дизъюнктов.
ТеоремарезолютивноговыводаТеоремаоополнотеполнотерезолютивноговыводаПРИМЕНЕНИЕМЕТОДАРЕЗОЛЮЦИЙЕслиЕслиSS��противоречиваяпротиворечиваясистемасистемадизъюнктов,дизъюнктов,тотоизизSSрезолютивнорезолютивновыводимвыводимпустойпустойдизъюнктдизъюнкт⇤.⇤.Пример.ПРИМЕНЕНИЕ МЕТОДА РЕЗОЛЮЦИЙ Рассмотрим формулу '✓⇣8x8y 9v 8u(A(u, v ) ! B(y , u))&◆⌘(¬9wA(w , u) ! 8zA(z, v ))! 9yB(x, y )РешениеПРИМЕНЕНИЕМЕТОДАЭтап 1. Покажем, чтоформула '1 РЕЗОЛЮЦИЙ= ¬' противоречивая.ПРИМЕНЕНИЕМЕТОДАРЕЗОЛЮЦИЙЗадача✓ ⇣'1 = ¬8x8y 9v 8u(A(u, v ) ! B(y , u)) &Проверить, верно ли, что |= '.РешениеРешениеРешение◆⌘(¬9wA(w , u) ! 8zA(z, v ))! 9yB(x, y ) Этап2. Приведем'1 МЕТОДАк ПНФ '2 .Методомрезолюций.ПРИМЕНЕНИЕРЕЗОЛЮЦИЙЭтап2.
Приведем'1 к ПНФ '2 . Переименование переменныхИсходная формула✓⇣✓ 0¬8x8y 9v 8u ⇣(A(u, v ) ! B(y 0 , u)) &Решение¬8x8y 9v 8u(A(u, v ) ! B(y , u)) &◆⌘◆0000⌘Этап2.Приведем'кПНФ'.(¬9wA(w, u) 2! 8zA(z,v ))! 9y B(x, y )1МЕТОДАПРИМЕНЕНИЕРЕЗОЛЮЦИЙ(¬9wA(w , u) ! 8zA(z, v ))! 9yB(x, y ) Удаление импликаций✓⇣¬8x¬8y 0 9v 8u(¬A(u, v ) _ B(y 0 , u)) &Решение◆⌘0000Этап 2. Приведем '1(¬¬9wA(wк ПНФ '2, .u) _ РЕЗОЛЮЦИЙ8zA(z, v ))_ 9y B(x, y )ПРИМЕНЕНИЕМЕТОДАПродвижение отрицаний✓⇣0 9v 8u9x8y(¬A(u, v ) _ B(y 0 , u)) &Решение◆⌘Этап 2.
Приведем(9wA(w'1 к ПНФ'.00002, u) _ 8zA(z, v ))& 8y ¬B(x, y )Вынесение кванторов'2 =9x8y 0 9v 8u9w 8z8y 00✓ (¬A(u, v ) _ B(y 0 , u)) &(A(w , u) _ A(z, v )) &¬B(x, y 00 )◆ РешениеЭтап 3. Приведем '2 к ССФ '3 .ПРИМЕНЕНИЕ МЕТОДАРЕЗОЛЮЦИЙ✓'3 =8y 08z8y 008uРешение(¬A(u, f (y 0 )) _ B(y 0 , u)) &(A(g (y 0 , u), u) _ A(z, f (y 0 ))) & ◆¬B(c, y 00 )Этап 4. Формирование системы дизъюнктов S' .S' =nD1 = ¬A(u, f (y 0 )) _ B(y 0 , u),ПРИМЕНЕНИЕD2 МЕТОДА= A(g (y 0 , u), u)РЕЗОЛЮЦИЙ_ A(z, f (y 0 )), oРешениеD3 = ¬B(c, y 00 ) Этап 5.
Резолютивный вывод из S' .S' =nD1 = ¬A(u, f (y 0 )) _ B(y 0 , u),D2 = A(g (y 0 , u), u) _ A(z, f (y 0 )), oD3 = ¬B(c, y 00 )1. D10 = ¬A(u1 , f (y10 )) _ B(y10 , u1 ), (вариант D1 )2. D20 = A(g (y20 , u2 ), u2 ) _ A(z2 , f (y20 )), (вариант D2 )ПРИМЕНЕНИЕРЕЗОЛЮЦИЙ3. D30 = A(g (y30 , fМЕТОДА(y30 )), f (y30 )), (склейкаD20 )4. D40 = B(y40 , g (y40 , f (y40 ))), (резольвента D10 и D30 )5. D50 = ¬B(c, y500 ), (вариант D3 )6. D60 = ⇤ . (резольвента D40 и D50 )Решение Заключение.
Успешный резолютивный вывод из S' означает,что S' � противоречивая система дизъюнктов.Значит, '1 = ¬' � невыполнимая формула.Значит, ' � общезначимая формула, |= '. 4. Логическое программирование. Декларативная семантика и операционнаясемантика; соотношение между ними. Стандартная стратегия выполненияХОРНОВСКИЕЛОГИЧЕСКИЕ ПРОГРАММЫлогических программ. Синтаксис логических программПусть = hConst, Func, Predi � некоторая сигнатура, вкоторой определяются термы и атомы.�заголовок� ::= �атом��тело� ::= �атом� | �тело�, �атом��правило� ::= �заголовок��тело�;�факт� ::= �заголовок�;�утверждение� ::= �правило� | �факт��программа� ::= �пусто� | �утверждение� �программа�ХОРНОВСКИЕЛОГИЧЕСКИЕ ПРОГРАММЫ�запрос� ::= ⇤ | ? �тело�ТерминологияПусть G =?C1 , C2 , .
. . , Cm � запрос. ТогдаIIатомы C1 , C2 , . . . , Cm называются подцелями запроса G ,mSпеременные множестваVarCi называются целевымипеременными ,IIi=1запрос ⇤ называется пустым запросом ,запросы будем также называть целевыми утверждениями .ХОРНОВСКИЕЛОГИЧЕСКИЕПРОГРАММЫДля удобства обозначенияусловимся в дальнейшемфакты A;ХОРНОВСКИЕЛОГИЧЕСКИЕПРОГРАММЫрассматривать как ЛОГИЧЕСКИЕправила A ; с заголовкомA и пустымХОРНОВСКИЕПРОГРАММЫтелом.Какнужно понимать логические программы?Как нужно понимать логические программы?Какнужнопониматьлогическиепрограммы?Главнаяособенностьлогическогопрограммирования�Главнаяособенность: логического� имеетполисемантичностьодна и та жепрограммированиялогическая программаГлавнаяособенность: одналогическогопрограммирования� имеетполисемантичностьитажелогическаяпрограммадве равноправные семантики, два смысла.полисемантичность: одна и тадваже смысла.логическая программа имеетдверавноправные семантики,Человек–программисти компьютер–вычислительимеют дведверавноправныесемантики,двасмысла.Человек–программистикомпьютер–вычислительимеютдверазные точки зрения на программу.Человек–программисткомпьютер–вычислитель имеют дверазные точки зрения наи программу.Программистуважнонапонимать,ЧТО вычисляет программа.разныеточки зренияпрограмму.Программистуважнопонимать,ЧТО вычисляетпрограмма.Такое пониманиепрограммыназываетсядекларативнойПрограммистуважнопонимать,ЧТОвычисляетпрограмма.Такоепониманиепрограммы называется декларативнойсемантикойпрограммы.Такоепониманиепрограммы называется декларативнойсемантикойпрограммы.семантикойКомпьютерупрограммы.важно �знать�, КАК проводить вычислениеКомпьютеруважно�знать�, КАКпроводитьвычислениепрограммы.
Такое пониманиепрограммыназываетсяКомпьютеруважнопонимание�знать�, КАКпроводитьвычислениепрограммы.Такоепрограммыназываетсяоперационной семантикой программы.программы.Такоепониманиепрограммы называетсяоперационнойсемантикойпрограммы.операционной семантикой программы.ХОРНОВСКИЕ ЛОГИЧЕСКИЕ ПРОГРАММЫКак нужно понимать логические программы?Декларативная семантикаОперационная семантикаПравило A0A1 , A2 , . . . , An ;Если выполнены условия Чтобы решить задачу A0 ,A1 , A2 , . . .
, An , то справедли- достаточно решить задачиво и утверждение A0 .A1 , A2 , . . . , An .Факт A0 ;Утверждение A0 считается Задача A0 объявляется реверным.шенной.Запрос ?C1 , C2 , . . . , CmПри каких значениях целевых РешитьсписокзадачпеременныхбудутвернывсеC,C,...,C.12mДЕКЛАРАТИВНАЯ СЕМАНТИКАотношенияCm ?1 , C2 , . . .
, семантикБолеестрогоеCописаниетребует привлеченияаппарата математической логики.Логические программы и логические формулыКаждому утверждению логической программы сопоставимлогическую формулу:Правило: D 0 = A0A1 , A2 , . . . , AnD 0 = 8X1 . . . 8Xk (A1 &A2 & . . . &An ! A0 ), где {X1 , . . . , Xk } =Факт: D 00 = AD 00 = 8X1 . . . 8Xk A, где {X1 , . . . , Xk } = VarAДЕКЛАРАТИВНАЯ СЕМАНТИКАЗапрос: G = ? C1 , C2 , .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
