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

Описание файла

Файл "LectLog16" внутри архива находится в папке "Старые лекции, в целом тоже самое". PDF-файл из архива "Старые лекции, в целом тоже самое", который расположен в категории "лекции и семинары". Всё это находится в предмете "математическая логика и логическое программирование" из седьмого семестра, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст 2 страницы из PDF

е. не существует алгоритма (машиныТьюринга), способного вычислить следующую функцию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является ли заданная формула ϕ логическим следствиемзаданного множества формул Γ?КОНЕЦ ЛЕКЦИИ 16..

Свежие статьи
Популярно сейчас