Ещё одни лекции В.А. Захарова, страница 4

Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима. Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.I |= ϕПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима. Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.I |= ϕI |= ∀x (P(x) → R(x)) I |= ∀x P(x) → ∀x R(x)ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима.

Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.I |= ϕI |= ∀x (P(x) → R(x)) I |= ∀x P(x) → ∀x R(x)I |= ∀x P(x)I |= ∀x R(x)ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима.

Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.I |= ϕI |= ∀x (P(x) → R(x)) I |= ∀x P(x) → ∀x R(x)I |= ∀x P(x)I |= ∀x R(x)I |= R(x)[d]ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима. Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.I |= ϕI |= ∀x (P(x) → R(x)) I |= ∀x P(x) → ∀x R(x)I |= ∀x P(x)I |= ∀x R(x)I |= R(x)[d]I |= (P(x) → R(x))[d]ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима. Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.I |= ϕI |= ∀x (P(x) → R(x)) I |= ∀x P(x) → ∀x R(x)I |= ∀x P(x)I |= ∀x R(x)I |= R(x)[d]I |= (P(x) → R(x))[d]I |= P(x)[d]ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима.

Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.I |= ϕI |= ∀x (P(x) → R(x)) I |= ∀x P(x) → ∀x R(x)I |= ∀x P(x)I |= ∀x R(x)I |= R(x)[d]I |= (P(x) → R(x))[d]I |= P(x)[d]I |= R(x)[d]Получили противоречие. Значит, контрмодели I не существует.ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∀x (P(x) → R(x)) → (∀x P(x) → ∀x R(x)) .Предположим, что ϕ необщезначима.

Тогда должнасуществовать интерпретация I (контрмодель), опровергающаяϕ. Изучим эту контрмодель.I |= ϕI |= ∀x (P(x) → R(x)) I |= ∀x P(x) → ∀x R(x)I |= ∀x P(x)I |= ∀x R(x)I |= R(x)[d]I |= (P(x) → R(x))[d]I |= P(x)[d]I |= R(x)[d]Получили противоречие.

Значит, контрмодели I не существует.Значит, |= ϕ.ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима. Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима. Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I |= ∃x (P(x) → ∀x P(x))ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима.

Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I |= ∃x (P(x) → ∀x P(x))I |= ∃x (P(x) I |= ∀x P(x)ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима. Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I |= ∃x (P(x) → ∀x P(x))I |= ∃x (P(x) I |= ∀x P(x)I |= P(x)[d1 ]ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима. Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I |= ∃x (P(x) → ∀x P(x))I |= ∃x (P(x) I |= ∀x P(x)I |= P(x)[d1 ]I |= P(x)[d2 ]ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛПример.Проверить общезначимость формулыϕ = ∃x (P(x) → ∀x P(x)) .Предположим, что ϕ необщезначима. Тогда существуетинтерпретация I (контрмодель), которая опровергает ϕ.I |= ∃x (P(x) → ∀x P(x))I |= ∃x (P(x) I |= ∀x P(x)I |= P(x)[d1 ]I |= P(x)[d2 ]Противоречия нет.I = DI , Pred: DI = {d1 , d2 }, P(d1 ) = true, P(d2 ) = false,I |= ϕ.Следовательно, |= ϕ.СЕМАНТИЧЕСКИЕ ТАБЛИЦЫПопробуем систематизировать этот способ проверкиобщезначимости формул.Общезначимость формулы доказываем «от противного»,пытаясь построить контрмодель.Контрмодель строим, указывая, какие формулы должны вней выполняться, а какие нет.

Требования(не)выполнимости формул, предъявляемые к контрмодели,сводим в таблицу и последовательно их уточняем.Если требования, которые предъявляются к контрмодели,оказываются несовместными, значит, проверяемаяформула неопровержима, т. е. общезначима.СЕМАНТИЧЕСКИЕ ТАБЛИЦЫСемантическая таблица — это упорядоченная пара множествформул Γ ; Δ , Γ, Δ ⊆ Form.Γ — это множество формул, которые мы хотим считатьистинными,Δ — это множество формул, которые мы хотим считатьложными.Пусть {x1 , x2 , . . . , xn } — множество свободных переменных вформулах множеств Γ, Δ.Семантическая таблица Γ ; Δ называется выполнимой ,если существует такая интерпретация I и такой набор значенийd1 , d2 , . . . , dn ∈ DI свободных переменных, для которыхI |= ϕ(x1 , x2 , . .

. , xn )[d1 , d2 , . . . , dn ] для любой формулы ϕ,ϕ ∈ Γ,I |= ψ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] для любой формулы ψ,ψ ∈ Δ.СЕМАНТИЧЕСКИЕ ТАБЛИЦЫПримерыСемантическая таблицаT = {∃x P(x), ¬P(y )} ; {∀xP(x), P(x) & ¬P(x)} выполнима. Ее выполнимость подтверждает интерпретацияI = DI , Pred: DI = {d1 , d2 }, P(d1 ) = true, P(d2 ) = false, инабор d1 , d2 значений свободных переменных x, y.Семантическая таблицаT = ∅ ; {∃y ∀xR(x, y ) → ∀x∃yR(x, y )} невыполнима. Почему?СЕМАНТИЧЕСКИЕ ТАБЛИЦЫТеорема (о табличной проверке общезначимости)|= ϕ ⇐⇒ таблица Tϕ = ∅ ; {ϕ} невыполнима.Доказательство. |= ϕ ⇐⇒ для любой интерпретации I и длялюбого набора d1 , .

. . , dn ∈ DI значений свободных переменныхx1 , . . . , xn имеет место I |= ϕ(x1 , . . . , xn )[d1 , . . . , dn ] ⇐⇒таблица Tϕ = ∅ ; {ϕ} невыполнима ни в однойинтерпретации.СЕМАНТИЧЕСКИЕ ТАБЛИЦЫСемантическая таблица Γ ; Δ , у которой Γ ∩ Δ = ∅,называется закрытой .УтверждениеЗакрытая таблица невыполнима.Доказательство.

Самостоятельно.Семантическая таблица Γ ; Δ , у которой множества Γ, Δсостоят только из атомарных формул, называется атомарной .УтверждениеНезакрытая атомарная таблица выполнима.Доказательство. Самостоятельно.СЕМАНТИЧЕСКИЕ ТАБЛИЦЫТаким образом, для доказательства общезначимости |= ϕдостаточно разработать систему правил, позволяющихпреобразовывать семантическую таблицу Tϕ = ∅ ; {ϕ} кзакрытым таблицам.Доказательства такого вида называются логическим выводом .Если в выводе участвуют семантические таблицы, тологический вывод называется табличным .Чтобы табличный вывод был корректным, правилапреобразования таблиц (правила табличного вывода ) должнысохранять выполнимость семантических таблиц.Поэтому начнем с разработки правил табличного вывода ипроверки их корректности.КОНЕЦ ЛЕКЦИИ 3.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. Захаровzakh@cs.msu.suhttp://mathcyb.cs.msu.su/courses/logprog.htmlЛекция 4.Подстановки.Табличный вывод.Корректность табличного вывода.ПОДСТАНОВКИПодстановка — это всякое отображение θ : Var → Term,сопоставляющее каждой переменной некоторый терм.Подстановки нужны для того, чтобы иметь возможностьпереходить от общих утверждений ∀x∀yP(x, y ) к их частнымвариантам P(f (z), c).Множество Domθ = {x : θ(x) = x} называется областьюподстановки .

Если область подстановки — это конечноемножество переменных, то такая подстановка называетсяконечной. Множество конечных подстановок обозначим Subst .Если θ ∈ Subst и Domθ = {x1 , x2 , . . . , xn }, то подстановка θоднозначно определяется множеством пар{x1 /θ(x1 ), x2 /θ(x2 ), .

. . , xn /θ(xn )}.Каждая пара xi /θ(xi ) называется связкой .ПОДСТАНОВКИДля заданного логического выражения E и подстановки θзапись E θ обозначает результат применения подстановки θ к E ,который определется так:Если E = x, x ∈ Var , то E θ = θ(x);Если E = c, c ∈ Const, то E θ = c;Если E = f (t1 , t2 , . . . , tk ), то E θ = f (t1 θ, t2 θ, . . . , tn θ);Если E = P(t1 , t2 , . . . , tk ), то E θ = P(t1 θ, t2 θ, . . . , tn θ);Если E = ϕ&ψ, то E θ = ϕθ & ψθ(аналогично для формул ϕ ∨ ψ, ϕ → ψ, ¬ϕ);Если E = ∀x0 ϕ, то E θ = ∀x0 (ϕθ ), где η — новаяподстановка, удовлетворяющая условиюx0 , если x = x0 ,θ (x) =θ(x), если x = x0 ,(аналогично для формул ∃x0 ϕ).ПОДСТАНОВКИПримерϕ : ∀x(P(x) → ¬R(y )) → R(f (x)) ∨ ∃yP(y )θ = { x/g (x, c), y /x, z/f (z) }Выделяются все свободные вхождения переменных в ϕϕ : ∀x(P(x) → ¬R(y )) → R(f (x)) ∨ ∃yP(y )К свободным вхождениям переменных применяется θϕθ : ∀x(P(x) → ¬R(x)) → R(f (g (x, c))) ∨ ∃yP(y )ПОДСТАНОВКИВ результате применения некоторых подстановок смыслутверждений (формул) может значительно исказиться.«Если у каждого есть дед, то у субъекта x тоже есть дед»ϕ(x) : ∀x∃yP(x, y ) → ∃yP(x, y )Очевидно, |= ϕ(x)Применим к ϕ(x) подстановку θ = { x/y }ϕ(x)θ : ∀x∃yP(x, y ) → ∃yP(y , y )«Если у каждого есть дед, то есть и такие, которые приходятсядедом самим себе»Очевидно, |= ϕ(x)θКак странно: общее утверждение ϕ(x) верно, а его частныйслучай ϕ(x)θ — нет.ПОДСТАНОВКИПеременная x называется свободной для терма t в формулеϕ(x), если любое свободное вхождение переменной x вформуле ϕ(x) не лежит в области действия ни одногоквантора, связывающего переменную из множества Vart .Подстановка θ = { x1 /t1 , .

. . , xn /tn } называется правильной дляформулы ϕ, если для любой связки xi /ti переменная xiсвободна для терма ti в формуле ϕ.ПримерПеременная y не является свободной для терма f (x, z) вформуле ϕϕ : ∀x(P(x) → ¬R(y )) → R(f (x)) ∨ ∃yP(y )А вот для терма f (y , z) переменная y в формуле ϕ свободна.ТАБЛИЧНЫЙ ВЫВОДПравила табличного вывода имеют видT0T1илиT0 ,T1, T2где T0 , T1 , T2 — семантические таблицы. Прочтение правилатаково:Таблица T0 выполнима тогда и только тогда, когдавыполнима таблица T1 (или T2 ).В тех случаях, когда таблица T0 редуцируется в пару таблицT1 , T2 , будем говорить, что правило имеет альтернативы.ТАБЛИЧНЫЙ ВЫВОДПравила табличного выводаL&Γ, ϕ&ψ|ΔΓ, ϕ, ψ|ΔL∨Γ, ϕ ∨ ψ|ΔR∨Γ, ϕ|Δ, Γ, ψ|ΔL→Γ|Δ, ϕ → ψΓ, ϕ → ψ|ΔR→Γ, ψ|Δ, Γ|ϕ, ΔΓ, ϕ|Δ, ψL¬Γ, ¬ϕ|ΔΓ|Δ, ϕR&R¬Γ|Δ, ϕ&ψΓ|Δ, ϕ, Γ | Δ, ψΓ|Δ, ϕ ∨ ψΓ|Δ, ϕ, ψΓ|Δ, ¬ϕΓ, ϕ|ΔТАБЛИЧНЫЙ ВЫВОДПравила табличного выводаL∀Γ, ∀xϕ(x)|ΔΓ, ∀xϕ(x), ϕ(x){x/t}|Δпеременная x свободна для терма tв формуле ϕ(x)R∀Γ|Δ, ∀xϕ(x)Γ|Δ, ϕ(x){x/c}константа c не содержится в формулахиз Γ, Δ и в формуле ϕ(x)ТАБЛИЧНЫЙ ВЫВОДПравила табличного выводаL∃Γ, ∃xϕ(x)|ΔΓ, ϕ(x){x/c}|Δконстанта c не содержится в формулахиз Γ, Δ и в формуле ϕ(x)R∃Γ|Δ, ∃xϕ(x)Γ|Δ, ∃xϕ(x), ϕ(x){x/t}переменная x свободна для терма tв формуле ϕ(x)ТАБЛИЧНЫЙ ВЫВОДЗачем нужны ограничения на подставляемые термыв правилах L∀, R∀, L∃, R∃?Если в правиле табличного вывода L∀ не придерживатьсяправильных подстановок, то выполнимая таблица− L∀ : ∀x∃yR(x, y ) | ∃yR(y , y ) ∀x∃yR(x, y ), ∃yR(y , y ) | ∃yR(y , y ) преобразуется в закрытую, т.е.

невыполнимую таблицу .Причина в том, что переменная x несвободна для терма y вформуле ∃yR(x, y ).ТАБЛИЧНЫЙ ВЫВОДЗачем нужны ограничения на подставляемые термыв правилах L∀, R∀, L∃, R∃?Если в правиле табличного вывода L∃ подставить «несвежую»константу, то выполнимая таблица− L∃ : ∃x P(x) | P(c) P(c) | P(c) преобразуется в закрытую, т.е. невыполнимую таблицу .Причина в том, что константа, подставляемая вместопеременной x, должна быть отлична от всех ранееиспользованных констант.ТАБЛИЧНЫЙ ВЫВОДОпределение табличного выводаТабличный вывод для таблицы T0 — это корневое дерево,вершинами которого служат семантические таблицы и при этом1) корнем дерева является таблица T0 ;Tyj?yT3yT0@@@TR yT@y1i@@@@@@R yT@R yT@2k?yT4ТАБЛИЧНЫЙ ВЫВОДОпределение табличного вывода2)из вершины Ti исходят дуги в вершины Tj (Tk )⇐⇒Ti— правило табличного вывода;Tj , (Tk )TyjL∃yT0@L→ @@TR yT@y1i@@R& @L∀ @@@R yT@R yT@2kR¬?yT3?yT4ТАБЛИЧНЫЙ ВЫВОДОпределение табличного вывода3) листьями дерева могут быть только закрытые иатомарные таблицы.TyjyT0@L→ @@TR yT@y1i@@R& @L∀ @@@R yT@R yT@2kL∃R¬?yT3закр.