Теормин (2006) (1162014), страница 4
Текст из файла (страница 4)
Тогда дизъюнкт D0 , являющийсярезольвентой D1 и D2 , таков, что D '0 - основной пример D0 .14Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)Теорема (полноты для резолюций): Если S – противоречивая система дизъюнктов, тосуществует резолютивное опровержение S.3. Логическое программированиеЛогическая программа – это совокупность формул, причем программа позволяет доказатьили опровергнуть общезначимость формул, которые в нее входят.Определение. Хорновским дизъюнктом называется дизъюнкт, в который входит не болееодной литеры без отрицания.Определение. Хорновская логическая программа – множество хорновских дизъюнктов.Определение. Запрос к программе – задача поиска всех правильных ответов в программе.Определение.
Ответом на запрос G : ? C1 ,..., Cm с целевыми переменными x1 , x2 ,..., xnназывается всякая подстановка θ ={x t ;...; x t }m11mОпределение. Ответ η на запрос к логической программе Р называется правильным, еслирезультат подстановки (C1 , C2 ,..., Cm )η является логическим следствием Р.Определение. Эрбрановская интерпретация I для логической программы Р называется еемоделью, если она является моделью для любого хорновского дизъюнкта, входящего в нее.Утверждение.
I – модель для логической программы Р тогда и только тогда, когда длялюбого основного примера D0 = A '0 ← A '1 & A '2 &...& A 'n , если любое A 'i принадлежит I, тои A '0 также принадлежит I.Лемма (о пересечении моделей): Пусть Р – хорновская логическая программа, а М' и М'' - еемодели. Тогда эрбрановская интерпретация М, являющаяся пересечением М' и М'' такжебудет моделью для Р.Следствие 1: пересечение произвольного числа моделей для Р также будет моделью.Следствие 2: пересечение всех моделей для Р также будет ее моделью.
Такая модель будетназываться наименьшей Н-моделью (ННМ) и обозначаться как M PТеорема: Пусть Р – хорновская логическая программа, С - основной терм. С являетсяследствием Р тогда и только тогда, когда он принадлежит ННМ Р.Определение. Пусть Р – хорновская логическая программа, D = A0 ← A1 & A2 &...& An некоторое ее программное утверждение, G : ? C1 ,..., Cm - запрос, а пересечение формальныхпараметров ( VarD ) с фактическими ( VarG ) пусто. Пусть Ci - подцель запроса G, аθ = НОУ (Сi , A0 ) . Тогда запрос G ' : ?(C1 ,..., Ci −1 , A1 , A2 ,..., An , Ci +1 ,..., Cm )θ , полученный из Gзаменой Ci на A1 , A2 ,..., An и последующей унификацией, называется SLD-резольвентойзапроса G и программного утверждения D с НОУ θ . При этом Ci называется выделеннойподцелью, а D – активизированным программным утверждением.15Математическая логика, сводка определений.
(с) 2006 GrGr (grgr@later.ru)Определение. SLD-резолютивным вычислением запроса G к хорновской логическойпрограмме Р называется последовательность пар (Gi ,θi ) , конечная или бесконечная, такая,что1) G0 = G2) Запрос Gi +1 - SLD-резольвента запроса Gi и варианта D' программного утверждения D,такого VarGi ∩ VarD ' = ∅ , а θi +1 - НОУ для этой резольвенты.3) Возможно три варианта вычисления:А) Gl = ? - успешное вычисление (SLD-резолютивное опровержение)Б) бесконечная последовательность – бесконечное вычислениеВ) обнаруживается, что очередную SLD-резольвенту построить нельзя – тупиковоевычисление.Определение.
Пусть (G1 ,θ1 ),..., (Gl −1 , θl −1 ), ( ,θl ) - успешное завершение запроса G кхорновской логической программе Р. Тогда подстановка θ = θ1θ 2 ...θ l | y1 , y2 ,..., yn называетсявычислимым ответом на запрос G к логической программе Р.Определение. Пусть Р – хорновская логическая программа. Тогда множеством успехов Рбудет называться следующее множество SuccP - это множество всех атомарных запросов,имеющих успешное SLD-резолютивное вычисление ( A ∈ BP - эрбрановскому базису Р).Определение. Пусть 2BP - множество всех подмножеств BP (множество всех эрбрановскихинтерпретаций). Оператором непосредственного следования для логической программы Рназывается функция TP : 2 BP → 2 BP , такая, что для любого подмножества BP (обозначим егоI) TP ( I ) = { A : A ∈ BP ; A ← A1 , A2 ,..., An } , где Аi принадлежит I – т.е. все то, что следует изинтерпретации I по правилам логической программы Р.Утверждение. Для оператора непосредственного следования выполняются свойства:I1 ⊆ I 2 ⇒ TP ( I1 ) ⊆ TP ( I 2 )TP ( I1 ∪ I 2 ) ⊇ TP ( I1 ) ∪ TP ( I 2 )I ∈ BP ; I |= P ⇔ TP ( I ) ⊆ IОпределение.
Интерпретация I называется неподвижной точкой операторанепосредственного следования, если выполняется равенство TP ( I ) = I . Множество всехнеподвижных точек оператора непосредственного следования обозначим как f pPОпределение. I 0 называется наименьшей неподвижной точкой оператора TP , есливыполняются 2 свойства:1) I 0 - неподвижная точка оператора TP ;2) для любой другой неподвижной точки I выполняется свойство I 0 ⊆ I .Наименьшая неподвижная точка обозначается как lf pP .Теорема (о неподвижных точках). В хорновской логической программе Р всегда∞существует наименьшая неподвижная точка, и lf pP = ∪ TPi (∅ ) = M P (т.е.
наименьшаяi =016Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)неподвижная точка равна объединению всех следствий конечной кратности и являетсянаименьшей эрбрановской моделью для логической программы Р).Теорема (корректности операционной семантики): Пусть Р – хорновская логическаяпрограмма, G – запрос к ней, θ - вычисленный ответ на запрос G к Р. Тогда вычисленныйответ θ - это правильный ответ.Следствие. SuccP ⊆ M P (т.е. множество успехов является подмножеством наименьшейэрбрановской модели).Определение.
Пусть Р – хорновская логическая программа, G0 - запрос к Р. Тогда квазиSLD-резолютивным вычислением запроса G0 к Р называется последовательность пар(G '1 , θ '1 ),..., (G 'n , θ 'n ), (G 'n +1 , θ 'n +1 ) , которая удовлетворяет требованию: еслиG 'n −1 = ? C1 ,..., Ci −1 , Ci , Ci +1 ,..., Cm , D : A0 ← A1 ,..., Ak ∈ P и θ 'n - произвольный унификатор Ci иA0 , то G 'n = ?(C1 ,..., Ci −1 , A1 ,..., Ak , Ci +1 ,..., Cm )θ 'n .Заметим, что SLD-резолютивное вычисление – частный случай квази-SLD-резолютивноговычисления, поэтому корректность квази-SLD-резолютивного вычисления представляетсобой отдельную теорему.Теорема (о квази-SLD-резолютивных вычислениях): Если атом С входит в наименьшуюэрбрановскую интерпретацию ( C ∈ M P ), то запрос G0 : ? C имеет успешное квази-SLDрезолютивное вычисление.Следствие.
Если C1 , C2 ,..., Cn ∈ M P , то запрос G : ? C1 , C2 ,..., Cn имеет успешное квази-SLDрезолютивное вычисление.Лемма (о подъеме для SLD-резолюций): Пусть G – запрос к хорновской логическойпрограмме Р, η - конечная подстановка, а запрос Gη имеет успешное квази-SLD-резолютивное вычисление Gη ,(G '1 ,θ '1 ),..., ( ,θ 'n ) . Тогда запрос G имеет успешное SLDрезолютивное вычисление G, (G1 ,θ1 ),..., ( , θ n ) , причем существует такая конечнаяподстановка ρ , что ηθ '1 θ '2 ...θ 'n = θ1θ 2 ...θ n ρ . Иначе говоря, результат частного случаязапроса для квази-SLD-резолютивного вычисления – это результат частного случая запросадля SLD-резолютивного вычисления.Теорема (о полноте; ван Эмдена): Если атом C ∈ M P , то C ∈ SuccP .Теорема (о полноте; Кларка): Пусть G – запрос к хорновской логической программе Р, θ правильный ответ на G.
Тогда существует вычисленный ответ η , такой, что для некоторойконечной подстановки ρ выполняется равенство θ = ηρ (т.е. любой правильный ответявляется частным случаем некоторого вычисленного ответа).Машина Тьюринга:Определение. Ленточный алфавит A = {a0 ,..., an } - это множество допустимых значенийячеек памяти (символ a0 называется пустым). Слово в алфавите А называется ленточнымсловом.Определение. Алфавит состояний Q = {q 0 , q1 ,..., qm ,...} - это множество состояний, причемсостояние q0 называется заключительным, а состояние q1 - начальным.17Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)Определение. Ленточная конфигурация – это тройка d =< w1 , q, w2 > , где w1 - ленточноеслово, которое является содержимым ленты слева от обозреваемой ячейки, q - текущеесостояние машины Тьюринга, w2 - слово, состоящее из самой ячейки и содержимого лентысправа от нее.Определение.
Команда машины Тьюринга – это пятерка < q, a, b, q ', D > , где q и q' –состояния, a, b – символы из алфавита А, D ∈ {L, R} .Определение. Машиной Тьюринга называется тройка T =< A, QT , ΠT > , где А – ленточныйалфавит, QT – конечное подмножество множества состояний, ПТ – множество команд.Важное ограничение: для любого состояния, отличного от заключительного, и символа изленточного алфавита существует единственная команда.Определение. Отношением непосредственного перехода называется отношение T : α → β ,*где α , β - состояния машины Тьюринга. Обозначим a ⎯⎯→ β транзитивное замыканиеTотношения непосредственного перехода.Для каждой машины Тьюринга определим функцию FT : q1 → q0 , причем если α - начальнаяконфигурация, то FT (α ) = β тогда и только тогда, когда β - заключительная конфигурация,*и a ⎯⎯→β .TТезис Чёрча: Для любой функции ϕ : q1 → q0 существует алгоритм вычисления этойфункции тогда и только тогда, когда ϕ = FT для некоторой машины Тьюринга.Введем дополнительные обозначения: nil – 0-местный функциональный символ (константа),• - 2-местный функциональный символ, и введем отображение множества машин Тьюрингана множество логических программ: Compile : T → PТеорема.
Пусто Т – машина Тьюринга, Compile(T ) = P - логическая программа. Тогда длялюбой начальной конфигурации α 0 =< ai1 ,..., aik ; q1 ; b j1 ,..., b jn > существует заключительная*конфигурация β 0 =< a 'l1 ,..., a 'lm ; q0 ; b 'r1 ,..., b 'rt > , такая, что a ⎯⎯→ β , тогда и только тогда,Tкогда запрос Gα 0 : ? R (•( aik , •( aik −1 ,..., ( ai1 , nil )...), q1 , •(b j1 ,..., (b jn , nil )...)) имеет успешное SLDрезолютивное вычисление с ответом{}η = u •(a ' , •(...(a ' , nil )...) ; v q ; w •(b ' , •(...(b ' , nil )...)) .lml10r1rtТеорема (Чёрча; о неразрешимости проблемы общезначимости для классическойлогики предикатов): Не существует алгоритма, который для любой формулы ϕ позволялбы проверить ее общезначимость, т.е. не существует алгоритма, который выдавал бы навыходе 1, если формула ϕ общезначима, и 0 в противном случае.Определение. Правилом выбора подцелей называется отображение R : ? C1 ,..., Cn → Ci (т.е.отображение, показывающее, какой атом должен быть выбран на текущем этапевычисления).Определение.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
