LectLog4 (2) (Старые лекции, в целом тоже самое)

Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. Захаров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 не является свободной для терма в формуле ϕϕ : ∀x(P(x) → ¬R(y )) → R(f (x)) ∨ ∃yP(y )ПОДСТАНОВКИПеременная 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 в формуле ϕ свободна.ПОДСТАНОВКИПеременная 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)ТАБЛИЧНЫЙ ВЫВОДПравила табличного вывода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)ТАБЛИЧНЫЙ ВЫВОДПравила табличного вывода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∀, R∀, L∃, R∃?Если в правиле табличного вывода L∀ не придерживатьсяправильных подстановок, товыполнимая таблица− L∀ :h ∀x∃yR(x, y ) | ∃yR(y , y ) iТАБЛИЧНЫЙ ВЫВОДЗачем нужны ограничения на подставляемые термыв правилах 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преобразуется в закрытую, т.е.

невыполнимую таблицу .ТАБЛИЧНЫЙ ВЫВОДЗачем нужны ограничения на подставляемые термыв правилах 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∀, R∀, L∃, R∃?Если в правиле табличного вывода L∃ подставить «несвежую»константу, товыполнимая таблица− L∃ :h ∃x P(x) | P(c) iТАБЛИЧНЫЙ ВЫВОДЗачем нужны ограничения на подставляемые термыв правилах L∀, R∀, L∃, R∃?Если в правиле табличного вывода L∃ подставить «несвежую»константу, товыполнимая таблица− L∃ :h ∃x P(x) | P(c) ih P(c) | P(c) iпреобразуется в закрытую, т.е.

невыполнимую таблицу .ТАБЛИЧНЫЙ ВЫВОДЗачем нужны ограничения на подставляемые термыв правилах L∀, R∀, L∃, R∃?Если в правиле табличного вывода L∃ подставить «несвежую»константу, товыполнимая таблица− L∃ :h ∃x P(x) | P(c) ih P(c) | P(c) iпреобразуется в закрытую, т.е. невыполнимую таблицу .Причина в том, что константа, подставляемая вместопеременной x, должна быть отлична от всех ранееиспользованных констант.ТАБЛИЧНЫЙ ВЫВОДОпределение табличного выводаТабличный вывод для таблицы T0 — этоТАБЛИЧНЫЙ ВЫВОДОпределение табличного выводаТабличный вывод для таблицы T0 — это корневое дерево,y@@@Ry@@@y@@y?y@Ry@?y@Ry@ТАБЛИЧНЫЙ ВЫВОДОпределение табличного выводаТабличный вывод для таблицы T0 — это корневое дерево,вершинами которого служат семантические таблицы и при этомTyj?yT3yT0@@@TR yT@y1i@@@@@@R yT@R yT@2k?yT4ТАБЛИЧНЫЙ ВЫВОДОпределение табличного выводаТабличный вывод для таблицы 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→ @@TR yT@y1i@@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 ).КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыРассмотрим правилоL →:hΓ, ϕ → ψ|∆i.hΓ, ψ|∆i, hΓ|ϕ, ∆iКОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ϕ → ψ|∆i.hΓ, ψ|∆i, hΓ|ϕ, ∆iТаблица hΓ, ϕ → ψ|∆i выполнима ⇐⇒Рассмотрим правилоL →:КОРРЕКТНОСТЬ ТАБЛИЧНОГО ВЫВОДАДоказательство леммыhΓ, ϕ → ψ|∆i.hΓ, ψ|∆i, hΓ|ϕ, ∆iТаблица hΓ, ϕ → ψ|∆i выполнима ⇐⇒существует интерпретация I и набор d̄ = hd1 , .