LectLog4 (1158000)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. Захаров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) 6= 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 (ϕθ0 ), где η — новаяподстановка, удовлетворяющая условиюx0 , если x = x0 ,0θ (x) =θ(x), если x 6= 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 )«Если у каждого есть дед, то есть и такие, которые приходятсядедом самим себе»Очевидно, 6|= ϕ(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&hΓ, ϕ&ψ|∆ihΓ, ϕ, ψ|∆iL∨hΓ, ϕ ∨ ψ|∆iR∨hΓ, ϕ|∆i, hΓ, ψ|∆iL→hΓ, ϕ → ψ|∆ihΓ|∆, ϕ → ψiR→hΓ, ψ|∆i, hΓ|ϕ, ∆ihΓ, ϕ|∆, ψiL¬hΓ, ¬ϕ|∆ihΓ|∆, ϕiR&R¬hΓ|∆, ϕ&ψihΓ|∆, ϕi, hΓ | ∆, ψihΓ|∆, ϕ ∨ ψihΓ|∆, ϕ, ψihΓ|∆, ¬ϕihΓ, ϕ|∆iТАБЛИЧНЫЙ ВЫВОДПравила табличного выводаL∀hΓ, ∀xϕ(x)|∆ihΓ, ∀xϕ(x), ϕ(x){x/t}|∆iпеременная x свободна для терма tв формуле ϕ(x)R∀hΓ|∆, ∀xϕ(x)ihΓ|∆, ϕ(x){x/c}iконстанта c не содержится в формулахиз Γ, ∆ и в формуле ϕ(x)ТАБЛИЧНЫЙ ВЫВОДПравила табличного выводаL∃hΓ, ∃xϕ(x)|∆ihΓ, ϕ(x){x/c}|∆iконстанта c не содержится в формулахиз Γ, ∆ и в формуле ϕ(x)R∃hΓ|∆, ∃xϕ(x)ihΓ|∆, ∃xϕ(x), ϕ(x){x/t}iпеременная x свободна для терма tв формуле ϕ(x)ТАБЛИЧНЫЙ ВЫВОДЗачем нужны ограничения на подставляемые термыв правилах L∀, R∀, L∃, R∃?Если в правиле табличного вывода L∀ не придерживатьсяправильных подстановок, то выполнимая таблица− L∀ :h ∀x∃yR(x, y ) | ∃yR(y , y ) ih ∀x∃yR(x, y ), ∃yR(y , y ) | ∃yR(y , y ) iпреобразуется в закрытую, т.е.

невыполнимую таблицу .Причина в том, что переменная x несвободна для терма y вформуле ∃yR(x, y ).ТАБЛИЧНЫЙ ВЫВОДЗачем нужны ограничения на подставляемые термыв правилах L∀, R∀, L∃, R∃?Если в правиле табличного вывода L∃ подставить «несвежую»константу, то выполнимая таблица− L∃ :h ∃x P(x) | P(c) ih P(c) | P(c) iпреобразуется в закрытую, т.е. невыполнимую таблицу .Причина в том, что константа, подставляемая вместопеременной 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¬?Ty3?yT4ТАБЛИЧНЫЙ ВЫВОДОпределение табличного вывода3) листьями дерева могут быть только закрытые иатомарные таблицы.TyjyT0@L→ @@R yT@Ty1i@@R& @L∀ @@@R yT@R yT@2kL∃атом.

табл.R¬?yT3закр. табл.?yT4закр. табл.ТАБЛИЧНЫЙ ВЫВОДОпределение табличного выводаТабличный вывод будем называть успешным (или табличнымопровержением ), если дерево вывода — конечное, и все листьядерева — закрытые таблицы.Существование успешного вывода означает, что корневаясемантическая таблица T0 невыполнима.Если T0 = h ∅ | ϕ i, то это означает, что |= ϕ.T0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) i(R →)?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) i(R →)?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) i(R →)?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) i(R →)?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) i(R →)?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) i(R∀)?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) i(R →)?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) i(R →)?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) i(R∀)?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) i(L∀)?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) i(R →)?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) i(R →)?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) i(R∀)?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) i(L∀)?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) i(L∀)?T5 = h ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) iT0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) i(R →)?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) i(R →)?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) i(R∀)?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) i(L∀)?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) i(L∀)?T5 = h ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) iPP(L →)PP)qPT6 = h∀x(P(x) → B(x)), |B(c)i T7 = h∀x(P(x) → B(x)), |B(c), P(c)i∀xP(x), B(c), P(c)∀xP(x), P(c)T0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) i(R →)?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) i(R →)?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) i(R∀)?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) i(L∀)?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) i(L∀)?T5 = h ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) iPP(L →)PP)qPT6 = h∀x(P(x) → B(x)), |B(c)i T7 = h∀x(P(x) → B(x)), |B(c), P(c)i∀xP(x), B(c), P(c)∀xP(x), P(c)T0 = h ∅ | ∀x(P(x) → B(x)) → (∀xP(x) → ∀xB(x)) i(R →)?T1 = h ∀x(P(x) → B(x)) | ∀xP(x) → ∀xB(x) i(R →)?T2 = h ∀x(P(x) → B(x)), ∀xP(x) | ∀xB(x) i(R∀)?T3 = h ∀x(P(x) → B(x)), ∀xP(x) | B(c) i(L∀)?T4 = h ∀x(P(x) → B(x)), ∀xP(x), P(c) | B(c) i(L∀)?T5 = h ∀x(P(x) → B(x)), P(c) → B(c), ∀xP(x), P(c) | B(c) iPP(L →)PP)qPT6 = h∀x(P(x) → B(x)), |B(c)i T7 = h∀x(P(x) → B(x)), |B(c), P(c)i∀xP(x), B(c), P(c)∀xP(x), P(c)закрытая таблицазакрытая таблицаT0 = h ∅ | ∃x(P(x) → ∀xP(x) iT0 = h ∅ | ∃x(P(x) → ∀xP(x) i(R →)?T1 = h ∃xP(x) | ∀xP(x) iT0 = h ∅ | ∃x(P(x) → ∀xP(x) i(R →)?T1 = h ∃xP(x) | ∀xP(x) i(L∃)?T2 = h P(c1 ) | ∀xP(x) iT0 = h ∅ | ∃x(P(x) → ∀xP(x) i(R →)?T1 = h ∃xP(x) | ∀xP(x) i(L∃)?T2 = h P(c1 ) | ∀xP(x) i(R∀)?T3 = h P(c1 ) | P(c2 ) iT0 = h ∅ | ∃x(P(x) → ∀xP(x) i(R →)?T1 = h ∃xP(x) | ∀xP(x) i(L∃)?T2 = h P(c1 ) | ∀xP(x) i(R∀)?T3 = h P(c1 ) | P(c2 ) iатомарная таблицаT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) i(R →)?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) i(R →)?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) i(L∀)?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) i(R →)?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) i(L∀)?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) i(R∃)?T3 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) i(R →)?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) i(L∀)?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) i(R∃)?T3 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) i(L∃)?T4 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | ∀y P(c2 , y ), ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) i(R →)?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) i(L∀)?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) i(R∃)?T3 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) i(L∃)?T4 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | ∀y P(c2 , y ), ∃x∀yP(x, y ) i(R∀)?T5 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | P(c2 , c4 ), ∃x∀yP(x, y ) iT0 = h ∅ | ∀y ∃xP(x, y ) → ∃x∀yP(x, y ) i(R →)?T1 = h ∀y ∃xP(x, y ) | ∃x∀yP(x, y ) i(L∀)?T2 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∃x∀yP(x, y ) i(R∃)?T3 = h ∀y ∃xP(x, y ), ∃xP(x, c1 ) | ∀yP(c2 , y ), ∃x∀yP(x, y ) i(L∃)?T4 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | ∀y P(c2 , y ), ∃x∀yP(x, y ) i(R∀)?T5 = h ∀y ∃xP(x, y ), P(c3 , c1 ) | P(c2 , c4 ), ∃x∀yP(x, y ) i?∞КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАЛемма о корректности правил выводаКаково бы ни было правило табличного выводаL&, R&, L∨, R∨, L →, R →, L¬, R¬, L∀, R∀, L∃, R∃T0 ,T1 , (T2 )таблица T0 выполнима тогда и только тогда, когдавыполнима таблица T1 (или выполнима таблица T2 ).КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ϕ → ψ|∆i.hΓ, ψ|∆i, hΓ|ϕ, ∆iТаблица hΓ, ϕ → ψ|∆i выполнима ⇐⇒существует интерпретация I и набор d̄ = hd1 , .

. . , dn i значенийсвободных переменных, для которых I |= Γ[d̄], I |= Γ[d̄],⇐⇒⇐⇒I 6|= ∆[d̄],I 6|= ∆[d̄],I |= (ϕ → ψ)[d̄]I |= ψ[d̄] или I 6|= ϕ[d̄]Рассмотрим правило⇐⇒ I |= Γ[d̄],I 6|= ∆[d̄],I |= ψ[d̄]L →: I |= Γ[d̄],илиI 6|= ∆[d̄],I 6|= ϕ[d̄]⇐⇒одна из таблиц T1 = hΓ, ψ|∆i или T2 = hΓ|ϕ, ∆i выполнима.КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыАналогично доказывается корректность остальных 7 правилдля логических связокКОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ∀x0 ϕ(x0 )|∆i.hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iТаблица hΓ, ∀x0 ϕ(x0 )|∆i выполнима ⇐⇒ существуетинтерпретация I и набор d1 , .

. . , dn значений свободныхпеременных, для которых I |= Γ[d1 , . . . , dn ],I 6|= ∆[d1 , . . . , dn ],Пусть d0 = t[d1 , . . . , dn ]. ТогдаI |= (∀x0 ϕ)[d1 , . . . , dn ]Рассмотрим правилоL∀:I |= (∀x0 ϕ)[d1 , . . . , dn ] ⇒ I |= ϕ[d0 , d1 , . . . , dn ] ⇒⇒ I |= ϕ[t[d1 , . . . , dn ], d1 , . . . , dn ] ⇒ I |= ϕ{x0 /t}[d1 , . . . , dn ].Следовательно, таблица hΓ, ∀x0 ϕ(x0 ), ϕ(x0 ){x0 /t}|∆iвыполнима в интерпретации I .На каком этапе доказательства существенно используется тотфакт, что переменная x0 свободна для терма t в формуле ϕ ?КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ∃xϕ(x)|∆i.hΓ, ϕ(x){x/c}|∆iОчевидно, что выполнимость таблицы hΓ, ϕ(x){x/c}|∆i влечетвыполнимость таблицы hΓ, ∃xϕ(x)|∆iРассмотрим правилоL∃:Допустим, что выполнима таблица hΓ, ∃xϕ(x)|∆i.

Характеристики

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций