Сводка определений - 2 (Старые варианты экзамена), страница 3

При этом f ( k ) называется сколемовской функцией.Определение. Система дизъюнктов S называется невыполнимой, если не существует такойинтерпретации, в которой будут выполнимы одновременно все дизъюнкты, входящие в S.Теорема. Формула ϕ общезначима тогда и только тогда, когда невыполнима системадизъюнктов S ¬ϕ .10Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)Определение.

Основным термом называется любой терм, не имеющий свободныхпеременных.Определение. Эрбрановским универсумом (Н) называется множество основных термов,которое строится следующим образом:⎧Constϕ1. H 0 = ⎨⎩ {a}2. H i +1 = H i ∪ { f ( k ) (t1 , t2 ,..., tk )} для всех f ( k ) ∈ Funcϕ и t1 , t2 ,..., tk ∈ H i∞3. H = ∪ H ii =0Определение. Эрбрановской интерпретацией для системы дизъюнктов Sϕ называетсяинтерпретация I =< H , Const, Func, Pred > , где H – эрбрановский универсум, а остальныемножества определяются следующим образом:Const : c ∈ Const; c = cFunc : f ( m ) ∈ Func; f(m): t1 , t2 ,..., tm ∈ Hf(m): (t1 , t2 ,..., tm ) → f ( m ) (t1 , t2 ,..., tm )Pred : P ( n ) ∈ PredТеорема (об эрбрановских интерпретациях): Система дизъюнктов невыполнима тогда итолько тогда, когда она невыполнима на эрбрановских интерпретациях.Существует несколько способов представления эрбрановских интерпретаций:1. Теоретико-множественный.Назовем основным атомом атомарную формулу (без свободных переменных), полученную врезультате подстановки в некоторый предикат Р основных термов:P(t1 , t2 ,..., tm ) ∈ Atom;(t1 , t2 ,..., tm ) ∈ HТогда I будет являться эрбрановской интерпретацией для множества основных атомов, еслина ней будет выполним любой основной атом из этого множества.2.

ПоследовательныйОсновной литерой называется либо основной атом, или его отрицание. Упорядоченноемножество всех основных атомов будет называться эрбрановским базисом В. Тогда сэрбрановской интерпретацией можно связать последовательность литер A1σ1 , A2σ 2 ,..., Alσ l ,... ,причем Aiσ i будет равно Ai , если Ai выполнима в I, и ¬Ai в противном случае.Определение. Пусть BH = { A1 , A2 ,..., Al ,...} - эрбрановский базис. Семантическим деревомназывается бинарное корневое дерево следующеговида (см. рисунок слева).В таком дереве каждая ветвь соответствует какойA1¬A1нибудь эрбрановской интерпретации.С помощью семантического дерева можно легкосформулировать критерии выполнимости системыдизъюнктов.A2¬A2 A2¬A2Определение.

Основным примером дизъюнкта D( x1 , x2 ,..., xn ) = L1 ∨ L2 ∨ ... ∨ Lm будетназываться подстановка D( x1 , x2 ,..., xn ){x t ,..., x t } , где t , t ,..., t ∈ H .n1n11112nМатематическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)Утверждение. Система дизъюнктов невыполнима тогда и только тогда, когда для любойэрбрановской интерпретации, которая задана в виде последовательности литер, существуеттакой основной пример D' дизъюнкта D из этой системы, чтоD '( x1 , x2 ,..., xn ) = L '1 ∨ L '2 ∨ ...

∨ L 'm , что для некоторых его компонент будет выполнятьсяσравенство L 'm = ¬A 'imim , т.е. всегда будет находиться ложный основной пример.Определение. Пусть v – вершина семантического дерева, в котором из корня ведет путь,помеченный литерами L1 , L2 ,..., Ln . Пусть также дизъюнкт D принадлежит системе Sϕ .Говорят, что дизъюнкт D опровергается в вершине v, если существует такой основнойпример D', состоящий из литер L '1 , L '2 ,..., L 'n , причем любая литера L 'i из D будет равна¬Li .Определение. Вершина v называется опровергающим узлом для системы дизъюнктов Sϕ ,если1) в вершине v опровергается какой-нибудь дизъюнкт D из Sϕ ;2) никакая другая вершина, лежащая выше на пути из корня к v не опровергает ниодного дизъюнкта.Лемма (о семантическом дереве): Система дизъюнктов невыполнима тогда и только тогда,когда в ее семантическом дереве каждая ветвь содержит опровергающий узел, и число такихузлов конечно.Лемма (Кенига): Если есть бесконечное семантическое дерево, и из каждой его вершинывыходит конечное число дуг, то это дерево содержит бесконечную ветвь.Теорема (Эрбрана; об основных примерах): Система дизъюнктов S невыполнима(противоречива) тогда и только тогда, когда существует конечное множество S' основныхпримеров дизъюнктов из S, такое, что S' – тоже противоречивое множество.Теорема Эрбрана сводит проблему выполнимости системы дизъюнктов к исследованиюистинности булевых формул.Алгоритм Девиса-Паттена проверки противоречивости системы дизъюнктов.1.

Строим семантическое дерево2. Порождаем основные примеры дизъюнктов из системы.После этого проверяется опровержимость основных примеров в вершине семантическогодерева. Алгоритм завершается успешно, если построенная система опровергающих узловпересекает все дерево.Определение. Композицией конечных подстановок θ и η называется такая конечнаяпостановка μ , что для любой переменной x μ ( x ) = ( xθ )η . Композиция подстановокобозначается как ηθ .Определение.

Подстановка θ называется унификатором для логических выраженийE1 , E2 ,..., En , если E1θ = E2θ = ... = Enθ .Определение. Подстановка θ называется наиболее общим унификатором (НОУ) длялогических выражений E1 , E2 ,..., En , если1) θ - унификатор для E1 , E2 ,..., En ;12Математическая логика, сводка определений.

(с) 2006 GrGr (grgr@later.ru)2) для любой подстановки η , которая тоже унифицирует E1 , E2 ,..., En найдется такаяподстановка ρ , что η = θρ (т.е. η является частным случаем θ ).⎧ t1 = s1⎪Определение. Наиболее общим унификатором для системы уравнений вида ⎨........... для⎪t = sm⎩mатомарных формул E1 = P(t1 , t2 ,..., tm ) и E2 = P( s1 , s2 ,..., sm ) называется такая подстановка θ ,что:⎧ t1θ = s1θ⎪1) выполняется система равенств ⎨ ........... ;⎪t θ = s θm⎩m2) любая другая подстановка, для которой эта система также выполняется, является частнымслучаем θ .Утверждение. θ - НОУ для формул E1 = P(t1 , t2 ,..., tm ) и E2 = P( s1 , s2 ,..., sm ) тогда и толькотогда, когда θ является НОУ для системы уравнений для этих формул.Лемма (о связке): Пусть x – переменная, а t – терм, причем х не является свободнойпеременной для t. Тогда если конечная подстановка θ является унификатором x и t (т.е.xθ = tθ ), то θ = { x } .tСледствие.

Подстановка θ из условия леммы является НОУ для x и t.⎧ x1 = t1⎪Теорема (о приведенной системе уравнений): Если ⎨ ........... - приведенная система⎪x = t⎩ m mуравнений, причем ни один x не является свободной переменной для любого t из системы, тоxxНОУ такой системы λ = 1 ,..., mt1tm{}Алгоритм унификации Мортелло-Мортанари⎧ t1 = s1⎪Дана система термальных уравнений ⎨...........

. Алгоритм решает ее методом подстановки.⎪t = sm⎩mДо тех пор, пока возможно, выполнить следующие действия:Выбрать произвольное уравнение и применить к нему одно из 6 правил:1) если уравнение имеет вид f (t '1 , t '2 ,..., t 'k ) = g ( s '1 , s '2 ,..., s 'k ) , то оно преобразовывается⎧ t '1 = s '1⎪в k уравнений ⎨ ........... ;⎪t ' = s 'k⎩ k2) если уравнение имеет вид f (t '1 , t '2 ,..., t 'k ) = g ( s '1 , s '2 ,..., s 'k ) , причем f ≠ g , тоалгоритм останавливается с ошибкой;3) если уравнение имеет вид c = k , где c и k – константы, или x=x, где х – переменная, тотакое уравнение надо удалить;13Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)4) если уравнение имеет вид t = y , где y – переменная, а t – терм, то это уравнениезаменяется на y = t ;5) если уравнение имеет вид y = si , причем y не является свободной переменной для si,но встречается в каких-нибудь уравнениях t j = s j , то в них надо произвести замену{ y }.si6) если уравнение имеет y = si , и при этом y является свободной переменной для si, тоалгоритм останавливается с ошибкой.Теорема: Алгоритм унификации завершается и работает корректно, т.е.:1.

для любой системы уравнений l алгоритм останавливается после применения к этойсистеме;2. если эта система унифицируема, то алгоритм выдает приведенную систему l’, такую,что ее НОУ совпадает с НОУ исходной системы;3. если эта система не унифицируема, то алгоритм останавливается с ошибкой.Определение. Правило резолюции для двух дизъюнктов D1 = D '1 ∨ L и D2 = D '2 ∨ ¬L и ихНОУ θ - это вывод их резольвенты – дизъюнкта вида D0 = ( D '1 ∨ D '2 )θ .Определение. Правило склеивания для дизъюнкта D = D '∨ L ∨ L ' и НОУ θ для L и L' – этовывод склейки D по паре L и L' – дизъюнкта вида D0 = ( D '∨ L)θ .Определение. Резолютивный вывод для системы дизъюнктов S – это такая конечнаяпоследовательность дизъюнктов D1 , D2 ,..., Dn , что для любого номера i>1 выполняется одноиз трех требований:1) Di - вариант D из S, т.е.

Di получен из D путем переименования переменных безотождествления;2) Di - резольвента двух дизъюнктов с меньшими номерами;3) Di - склейка дизъюнкта с меньшим номеромРезолютивный вывод называется успешным (резолютивным опровержением), если егопоследний дизъюнкт Dn - пустой.Лемма (о резолюции): Если D0 - резольвента дизъюнктов D и D', то он является ихлогическим следствием.Лемма (о склейке): Если D0 - склейка дизъюнкта D, то он является его логическимследствием.Теорема (корректности резолютивного вывода): Если D1 , D2 ,..., Dn - резолютивный выводиз семейства дизъюнктов S, то Dn - логическое следствие S.Лемма (о подъеме для резолюции): Пусть D '1 и D '2 - основные примеры дизъюнктов D1 иD2 соответственно, а D '0 - резольвента D '1 и D '2 .

Тогда дизъюнкт 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Определение.