Лекция 15. Алгоритмическая полнота логических программ. Моделирование машин Тьюринга ... (Лекции 2014), страница 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..