15. Алгоритмическая полнота логических программ. Моделирование машин Тьюринга логическим программами. Теорема Черча (В.А. Захаров - Лекции), страница 2

Речь идет об алгоритмически неразрешмыхзадачах.Например, интересен вопрос о том, можно ли по заданномузапросу G к логической программе P выяснить, имеет ли этотзапрос хотя бы одно успешное вычисление. Тогда не пришлосьбесполезно тратить время на построение дереваSLD-резолютивных вычислений.ТЕОРЕМА ЧЕРЧАТеорема Тьюринга об алгоритмическойнеразрешимости проблемы остановаПроблема останова машин Тьюринга алгоритмическинеразрешима, т. е. не существует алгоритма (машиныТьюринга), способного вычислить следующую функцию1, если x — это начальная ленточная конфигурация,если y — это список команд МТ π,F (x, y ) =и вычисление π(x) конечно;0 в противном случае.ДоказательствоИзвестно каждому первокурснику.ТЕОРЕМА ЧЕРЧАИз теоремы о моделировании машин Тьюринга логическимипрограммами и теоремы об алгоритмической неразрешимостипроблемы останова машин Тьюринга получаем нескольковажных следствийСледствие 1.Не существует алгоритма, способного определить по заданномузапросу G к хорновской логической программе P,Iявляется ли дерево SLD-резолютивных вычисленийзапроса G конечным;Iсодержит ли дерево SLD-резолютивных вычисленийзапроса G хотя бы одно успешное вычисление;Iявляется ли заданная подстановка θ вычисленным ответомна запрос G .ТЕОРЕМА ЧЕРЧАСледствие 2 (Теорема Черча).Не существует алгоритма, способного определить позаданной замкнутой формуле логики предикатов ϕ,является ли эта формула общезначимой, т.

е. проблемаобщезначимости "|= ϕ ?"алгоритмически неразрешима.ДоказательствоПусть G : ?C1 , . . . , Cm произвольный запрос к произвольнойлогической программе P = {D1 , . . . , DN }.Тогда...ТЕОРЕМА ЧЕРЧАДоказательствоЗапрос G к программе P имеет хотя бы одно успешноеSLD-резолютивное вычисление⇐⇒(теоремы корректности и полноты)Запрос G к программе P имеет хоть один правильный ответ θ⇐⇒(определение правильного ответа){D1 , . . . , DN } |= ∀z1 .

. . ∀zk (C1 & . . . &Cm )θ⇐⇒(теорема о логическом следовании)|= D1 & . . . &DN }∀z1 . . . ∀zk (C1 & . . . &Cm )θ.ТЕОРЕМА ЧЕРЧАТеорема Черча об алгоритмической неразрешимости проблемыобщезначимости показывает, что ни одна системаавтоматического доказательства теорем не можетгарантировать решение следующих вопросов для произвольныхформул:Iявляется ли заданная формула ϕ общезначимой?Iявляется ли заданная формула ϕ выполнимой?Iявляется ли заданная формула ϕ логическим следствиемзаданного множества формул Γ?КОНЕЦ ЛЕКЦИИ 15..