2. Логика высказываний - синтаксис, семантика, выполнимость, общезначимость, метод семантических таблиц, алгоритм DPLL (Лекции)

Математическая логикаЛектор:Подымов Владислав Васильевичe-mail:valdus@yandex.ru2017, весенний семестрЛекция 2Логика высказываний:синтаксис, семантика,выполнимость, общезначимостьМетод семантических таблицSATЛогика высказываний: вступлениеЧто такое логика высказываний?В логике высказываний на основеIIистинности “простых” высказываний и“примитивных” причинно-следственных связейанализируется истинность более “сложных” высказыванийНапример, можно рассмотреть такое предложение:Если будете прогуливать лекции,то ничего хорошего из этого не выйдетЛогика высказываний: вступлениеЧто такое логика высказываний?В логике высказываний на основеIIистинности “простых” высказываний и“примитивных” причинно-следственных связейанализируется истинность более “сложных” высказыванийНапример, можно рассмотреть такое предложение:Если будете прогуливать лекции,то ничего хорошего из этого не выйдетAМожно ли сказать, что это “простое высказывание”?Логика высказываний: вступлениеЧто такое логика высказываний?В логике высказываний на основеIIистинности “простых” высказываний и“примитивных” причинно-следственных связейанализируется истинность более “сложных” высказыванийНапример, можно рассмотреть такое предложение:Если будете прогуливать лекции,то ничего хорошего из этого не выйдетA→¬BЗдесь есть причинно-следственная связь .

. .Логика высказываний: вступлениеЧто такое логика высказываний?В логике высказываний на основеIIистинности “простых” высказываний и“примитивных” причинно-следственных связейанализируется истинность более “сложных” высказыванийНапример, можно рассмотреть такое предложение:Если будете прогуливать лекции,то ничего хорошего из этого не выйдетA→¬B. .

. между двумя простыми высказываниямиЛогика высказываний: вступлениеЧто такое логика высказываний?В логике высказываний на основеIIистинности “простых” высказываний и“примитивных” причинно-следственных связейанализируется истинность более “сложных” высказыванийНапример, можно рассмотреть такое предложение:Если будете прогуливать лекции,то ничего хорошего из этого не выйдетA→¬BА одно из высказываний можно сделать ещё прощеЛогика высказываний: вступлениеЧто такое логика высказываний?В логике высказываний на основеIIистинности “простых” высказываний и“примитивных” причинно-следственных связейанализируется истинность более “сложных” высказыванийНапример, можно рассмотреть такое предложение:Если будете прогуливать лекции,то ничего хорошего из этого не выйдетA→¬BЛогика высказываний: вступлениеЧто получилось после формализации высказывания?Что-то очень похожее на формулу булевой алгебры,но не совсем:Какой смысл имеет построенное высказывание?Булева алгебра:значение формулы — это булева функцияЛогика высказываний:?A0011B A → ¬B01110110Логика высказываний: вступлениеДля языка логики высказываний будут описаныалфавит: символы, используемые в языкесинтаксис: правила, по которым из символов строятсявысказывания языка (формулы)семантика: значение этих высказыванийЗатем будутIIIIстрого сформулированы интересующие нас свойстваформул (выполнимость, невыполнимость, общезначимость)описаны логические средства проверки этих свойств(метод семантических таблиц)показаны примеры сведения решения практических задач кпроверке сформулированных свойствпоказаны методы проверки этих свойств, используемые напрактике(DPLL)Алфавит, синтаксисАлфавитПропозициональные переменные VarЛогические связки&, ∨, →, ¬Скобки(, )1,2Синтаксис(это индуктивное определение)Что такое формула:I x — атомарная формула, или атом(x ∈ Var)I Составные формулы:(ϕ, ψ — формулы)(ϕ & ψ)(ϕ ∨ ψ)(ϕ → ψ)(¬ϕ)I других формул нет(этот пункт индуктивного определения будет опускаться)Приоритет связок: ¬, потом &, потом ∨, потом →Скобки можно опускать согласно приоритету1συντ αξισ (древнегреческий) — составление, построение, порядокОжегов.

Толковый словарь: Раздел грамматики — наука о законах соединения слови о строении предложений2СемантикаСемантика1 — это значение, смыслКак определить значение формулы?IIЗначения атомов задаются интерпретациейI : Var → {t, f}(t = true, f = false)Значение I (ϕ) составной формулы ϕ в интерпретации Iопределяется так:I (ϕ & ψ) = t ⇔ I (ϕ) = t и I (ψ) = tI (ϕ ∨ ψ) = t ⇔ I (ϕ) = t или I (ψ) = tI (ϕ → ψ) = t ⇔ I (ϕ) = f или I (ψ) = tI (¬ϕ) = t⇔ I (ϕ) = fВ логике принято использовать немного другие обозначения:I |= ϕ ⇔ I (ϕ) = tI 6|= ϕ ⇔ I (ϕ) = f1Ожегов, Шведова. Толковый словарь русского языкаСемантикаПримерVar = {A, B, .

. .}ϕ : A → ¬BI(A) = f, I(B) = tИмеет место следующее:I 6|= ¬B(так как I(B) = t)I |= A → ¬B (так как I(A) = f)Содержательное пояснениеA: высказывание “Я прогуливаю лекции”B: высказывание “Из этого выйдет что-то хорошее”I: мир, в котором я живуIII(A) = f: я прилежно хожу на лекцииI(B) = t: из этого выйдет что-то хорошееI |= A → ¬B: тот, кто сказал “Если я прогуливаю лекции, то изэтого не выйдет ничего хорошего”, правСемантикаПримерVar = {A, B, .

. .}ϕ : A → ¬BI(A) = f, I(B) = fИмеет место следующее:I |= ¬B(так как I(B) = f)I |= A → ¬B (так как I(A) = f)Содержательное пояснениеA: высказывание “Я прогуливаю лекции”B: высказывание “Из этого выйдет что-то хорошее”I: мир, в котором я живуIII(A) = f: я прилежно хожу на лекцииI(B) = f: из этого не выйдет ничего хорошегоI |= A → ¬B: тот, кто сказал “Если я прогуливаю лекции, то изэтого не выйдет ничего хорошего”, правСемантикаПримерVar = {A, B, .

. .}ϕ : A → ¬BI(A) = t, I(B) = tИмеет место следующее:I 6|= ¬B(так как I(B) = t)I 6|= A → ¬B (так как I(A) = t и I(¬B) = f)Содержательное пояснениеA: высказывание “Я прогуливаю лекции”B: высказывание “Из этого выйдет что-то хорошее”I: мир, в котором я живуIII(A) = t: я прогуливаю лекцииI(B) = t: из этого выйдет что-то хорошееI 6|= A → ¬B: тот, кто сказал “Если я прогуливаю лекции, то изэтого не выйдет ничего хорошего”, неправВыполнимость и общезначимостьКакие же свойства формул исследуются в логике высказываний?IIIФормула ϕ выполнима (||= ϕ1 ), если существуетинтерпретация I, такая что I |= ϕФормула ϕ невыполнима (6||= ϕ), если для любойинтерпретации I верно I 6|= ϕФормула ϕ общезначима (|= ϕ), если для любойинтерпретации I верно I |= ϕВстречались ли вам эти свойства формул раньше?1Логика высказыванийБулева алгебраϕ выполнимаϕ выполнимаϕ невыполнимаϕ≡0ϕ общезначимаϕ≡1Это необщеупотребимое обозначение, его придумал яВыполнимость и общезначимостьКак связаны между собой выполнимость, общезначимость иневыполнимость?формула ϕ выполнимаϕ=ψвыдать противоположный ответформула ψ невыполнимаψ = ¬χχ = ¬ψформула χ общезначимаПроверка каждого из этих свойств может быть легко сведенак проверке каждого другого свойстваМетод семантических таблицформула ϕ выполнимаϕ=ψвыдать противоположный ответформула ψ невыполнимаψ = ¬χχ = ¬ψформула χ общезначимаДалее рассматриваем задачупроверки общезначимости (булевых) формулМетод семантических таблицКак проверить общезначимость формулы ϕ?Булева алгебра: вычислить столбец значений реализуемойфункции и проверить, содержит ли он хотя бы один 0В терминах логики это перебор всех интерпретаций ивычисление значения ϕ в каждой из нихМожно ли сократить этот перебор?Да, и это основное назначение метода семантических таблиц:IIIпредположим, что формула ϕ необщезначима, и попробуемпостроить интерпретацию I, такую что I 6|= ϕна каждом шаге построения имеем формулы,предполагаемые истинными и ложными в I, и из готовыхпредположений получаем новые с “более простыми”формуламиесли все предположения привели к противоречивымтребованиям к I, то формула признаётся общезначимойМетод семантических таблицСемантическая таблица (логики высказываний) — это парамножеств формул: T = h Γ | ∆ iТаблица T выполнима, если существует интерпретация I, такаячто для любой формулы ϕ ∈ Γ верно I |= ϕ, а длялюбой формулы ψ ∈ ∆ верно I 6|= ψзакрыта, если Γ ∩ ∆ 6= ∅атомарна, если все формулы из Γ и ∆ атомарныСодержательное пояснение:Таблица T — это предположение о том, что формулы из Γистинны, а формулы из ∆ ложныВыполнимая таблица — это предположение, верное хотя бы водной интерпретацииЗакрытая таблица — это очевидно неверное предположениеАтомарная незакрытая таблица — это явное описаниеинтерпретаций I, в которых предположение верноМетод семантических таблицДля краткости будем опускать фигурные скобки в записимножеств семантической таблицыУтверждение|= ϕ ⇔ семантическая таблица h ∅ | ϕ i невыполнимаУтверждениеЛюбая закрытая таблица невыполнимаУтверждениеЛюбая незакрытая атомарная таблица выполнимаДоказательство.Самостоятельно (это очень просто)Метод семантических таблицЧтобы доказать общезначимость ϕ, достаточно разработатьправила преобразования таблиц, позволяющие свести неявноепротиворечие (невыполнимую таблицу) к явному противоречию(набору закрытых таблиц)Доказательства такого вида называются логическим выводомВывод, в котором участвуют семантические таблицы, принятоназывать табличным, а правила преобразования семантическихтаблиц — правилами табличного выводаКак же выглядят эти правила?Метод семантических таблицПравила табличного вывода имеют следующий вид:T0T0(*):(**):,,T1T1, T2где T0 , T1 , T2 — семантические таблицыПравила прочитываются так:(*): таблица T0 выполнима тогда и только тогда, когдавыполнима таблица T1(**): таблица T0 выполнима тогда и только тогда, когдавыполнима хотя бы одна из таблиц T1 , T2Таблицы T1 , T2 в (**) — это альтернативыМетод семантических таблицПравила табличного вывода для логики высказываний:L&h Γ, ϕ & ψ | ∆ ih Γ, ϕ, ψ | ∆ iR&h Γ | ∆, ϕ & ψ ih Γ | ∆, ϕ i, h Γ | ∆, ψ iL∨h Γ, ϕ ∨ ψ | ∆ ih Γ, ϕ | ∆ i, h Γ, ψ | ∆ iR∨h Γ | ∆, ϕ ∨ ψ ih Γ | ∆, ϕ, ψ iL→h Γ, ϕ → ψ | ∆ ih Γ, ψ | ∆ i, h Γ | ∆, ϕ iR→h Γ | ∆, ϕ → ψ ih Γ, ϕ | ∆, ψ iL¬h Γ, ¬ϕ | ∆ ih Γ | ∆, ϕ iR¬h Γ | ∆, ¬ϕ ih Γ, ϕ | ∆ iМетод семантических таблицТабличный вывод для таблицы T0 — это корневое дерево, такоечто:1.

его вершинам приписаны семантические таблицыT0TiT1R→TjL¬T3TkL&T4T2Метод семантических таблицТабличный вывод для таблицы T0 — это корневое дерево, такоечто:2. его корню приписана таблица T0T0TiT1R→TjL¬T3TkL&T4T2Метод семантических таблицТабличный вывод для таблицы T0 — это корневое дерево, такоечто:3. из Ti исходят дуги в Tj (и Tk ) ⇔Ti— правило табличного выводаTj , (Tk )T0L→TjL¬T3TiT1L∨R→TkL&T4T2Метод семантических таблицТабличный вывод для таблицы T0 — это корневое дерево, такоечто:4. метки его листьев — закрытые или атомарные таблицыT0L→TjL¬T3атом.таб.TiT1L∨R→TkL&T4атом.таб.T2закр.таб.Метод семантических таблицТабличный вывод успешен, если он конечен и все его листьяпомечены закрытыми таблицамиЗачем нужен успешный табличный вывод?Он показывает, что таблица, для которой он построен,невыполнимаЕсли он построен для таблицы h ∅ | ϕ i, то |= ϕУтверждениеЛюбой табличный вывод в логике высказыванийконеченДоказательство.Глубина вывода для таблицы h Γ | ∆ i не превосходит N + 1, гдеN — суммарное число связок в формулах из Γ, ∆HМетод семантических таблицПримеры табличного выводаh | A→A∨B iR→h A | A∨B iR&h A | A, B iзакрытая таблицаВывод успешен:|= A → A ∨ Bh | A∨B→A iR→h A∨B | A iL∨hA|AihB|Aiнезакрытая атомарная таблицаВывод неуспешен:6|= A ∨ B → AМетод семантических таблицЛемма корректности правил выводаКаково бы ни было правило табличного выводаL&, R &, L∨, R∨, L→, R→, L¬, R¬T0 ,T1 , (T2 )таблица T0 выполнима тогда и только тогда, когдавыполнима таблица T1 (или выполнима таблица T2 )Доказательство.Подробно остановимся только на правиле L→:h Γ, ϕ → ψ | ∆ ih Γ, ψ | ∆ i, h Γ | ∆, ϕ iПусть верхняя таблица выполнима: существует интерпретация I,такая что I |= χ0 для χ0 ∈ Γ, I 6|= χ00 для χ00 ∈ ∆, и I |= ϕ → ψТогда верно хотя бы одно из двух: I 6|= ϕ, I |= ψ — а значит,хотя бы одна из нижних таблиц выполнимаРассуждения в обратную сторону аналогичныHМетод семантических таблицТеорема о табличном выводе в логике высказыванийПусть D — табличный вывод для семантическойтаблицы T .

Тогда T невыполнима в том и только в томслучае, если D успешенДоказательство.Следует из леммы корректности правил табличного вывода,конечности табличного вывода и невыполнимости закрытыхтаблицСледствие|= ϕ ⇔ для таблицы h ∅ | ϕ i существует успешныйтабличный выводСледствие|= ϕ ⇔ все выводы для таблицы h ∅ | ϕ i успешныHSATформула ϕ выполнимаϕ=ψвыдать противоположный ответформула ψ невыполнимаψ = ¬χχ = ¬ψформула χ общезначимаТеперь рассматриваем задачупроверки выполнимости (булевых) формулSATisfiability(для экономии места будем опускать “ &”, а вместо ¬x писать x)(и еще будем писать 0/1 вместо true/false для значений переменных)SAT: приложенияЗачем столько внимания задаче SAT?Что “практически” полезного можно решить с её помощью?Приведём несколько примеров и областей и показать, какзадачи из этих областей сводятся к SATНо сначала несколько обозначений:I если exn — в точности все переменные формулы ϕ, тоIϕ : exn → {0, 1} — интерпретация, в которой выполняетсяформула ϕ:Iϕ |= ϕI ∃x ϕ — это формула ϕ0 ∨ ϕ1 , где ϕi получается из ϕподстановкой значения i на место переменной xI ϕ ↔ ψ — это сокращение для формулы ϕ → ψ & ψ → ϕSAT: приложенияПримерЖеня, Аня, Катя и Петя решили собраться вечером и поучитьлогику за чашкой кофеНеожиданно выяснилось, чтоI Женя по будням много работает, а по выходнымотсыпается, так что может встречаться только попонедельникам, средам и четвергамI у Ани по пятницам спецсеминарI Катя по средам вечером занимается плаваниемI а Петя по вторникам ходит на бокс, а каждый четверг пьётпиво со школьными друзьямиКогда же им собираться?ϕ : (Mon ∨ Wed ∨ Thu) Fri Wed Tue ThuФормула ϕ выполнима, и единственная интерпретация Iϕ :Iϕ (Mon) = 1, Iϕ (Tue) = · · · = Iϕ (Sun) = 0Значит, из всей недели только понедельник подходит для логикиSAT: приложенияПример: проверка достижимости вершины в графеvifДостижима ли вершина f из i?Закодируем вершины:i ∼ 00,v ∼ 01,f ∼ 10Перепишем задачу как набор формул:IIвершины i и f : I (x1 , x2 ) = x1 x2 , F (x1 , x2 ) = x1 x2описание дуг графа:R(x1 , x2 , x1 0 , x2 0 ) = x1 x2 x1 0 x2 0 ∨ x1 x2 x1 0 x2 0ϕ : I (x10 , x20 ) & R(x10 , x20 , x11 , x21 ) & R(x11 , x21 , x12 , x22 )&(F (x10 , x20 ) ∨ F (x11 , x21 ) ∨ F (x12 , x22 ))||= ϕ ⇔ f достижима из i в данном графе, а интерпретацией Iϕописывается путь из i в fSAT: приложенияПример: Bounded Model Checking (коротко и “на пальцах”)Рассмотрим программу π (или несколько взаимодействующихпрограмм), работающую над конечными данными,принимающими значения из области DМожно ли с помощью SAT убедиться, что заданные “плохие”состояния данных никогда не будут получены программой принедолгой (в пределах k шагов) работе?Добавим к данным значение счётчика команд: D 0 = D × PCОбъявим элементы D 0 вершинами графа и соединим так, какданные преобразуются выполнением инструкций программыНачальное и “плохие” состояния данных — это вершины графаПлохие состояния данных могут быть получены ⇔ хотя бы однаплохая вершина достижима из начальной в графеSAT: приложенияПример: проектирование схем (проверка эквивалентности)Рассмотрим две схемы из функциональных элементов:x1x2x1x2¬¬u2u1&u∨¬yyКак проверить, реализуют ли эти схемы одну и ту же функцию?Например, так:∃u1 ∃u2 ((y ↔ u1 ∨ u2 ) &(x1 ↔ ¬u1 ) &(x2 ↔ ¬u2 ))⊕∃u ((y ↔ ¬u) &(u ↔ x1 & x2 ))?≡0SAT: теория и практика решенияНасколько эффективно можно решать задачу SAT?Есть два взгляда на этот вопрос:IТеоретическийIIIКаковы наилучшие оценки сложности решающегоалгоритма?Где находится задача в иерархии классов сложности?ПрактическийIМожно ли написать программу, которая будет решатьзадачу за разумное время?SAT — яркий пример задачи, для которой возможностиэффективного решения сильно различаются стеоретической и практической точек зренияSAT: теория и практика решенияТеоретический взглядТеорема КукаSAT — NP-полная задачаНасколько это плохо для практического решения?IIЗадачу SAT можно решить1Время работы решающего алгоритма неразумно велико2Небольшая оговоркаКогда говорят о задаче SAT, часто имеют в виду проверкувыполнимости формул, представленных в конъюнктивнойнормальной форме (КНФ)Такое допущение не ограничивает общности задачи: можнобыстро привести произвольную формулу к КНФ1за полиномиальное время на недетерминированной машине Тьюрингаесли P 6= NP, то время работы неполиномиально; но если вдругокажется, что P = NP, то её могут научиться решать быстро2SAT: теория и практика решенияПрактический взглядДва основных “класса” эффективных решающих алгоритмов:DPLL1 , локальный поискДесятки программных средств(SAT-решателей, или SAT-солверов):MiniSAT, zChaff, RSat, Lingeling, WinSAT, .