МПЗиО_2_17_ЛогичТеории (1185821), страница 2

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

Текст из файла (страница 2)

и т. тогда, когда ееуниверсальное замыкание истинно)Свойства логики первого порядка? Полнота чистого ИП (теорема Гёделя,1929 г.): любомуистинному высказыванию P соответствует теорема в T Корректность: все теоремы общезначимы (истинны) Тем самым имеется однозназначная связь логич.истинности высказывания и его выводимости.19ИСЧИСЛЕНИЕ ПРЕДИКАТОВ:ДРУГИЕ СВОЙСТВАНеполнота некоторых прикладных ИП (в частности,Формальная арифметика – Гёдель,1930 г.):в них есть недоказуемые истинные утверждения.Причина : наличие аксиом с рекурсиейНепротиворечивость (формальная и содержательная)Неразрешимость (теорема Черча,1936 г.):не существует общего метода (алгоритма) установленияобщезначимости (тождественной истинности)произвольной формулы F ,т.е.

является ли она теоремой или нет.Полуразрешимость: есть процедура проверкиобщезначимости, которая для формулы-теоремы даетположительный ответ, а в случаеформулы-нетеоремы возможно зацикливание.20ИСЧИСЛЕНИЕ ПРЕДИКАТОВ:ДОКАЗАТЕЛЬСТВО ТЕОРЕМЗадача доказательства некоторой формулы F(теоремы), т.е. ее вывода из формул-аксиом А1, … , Anсводится к выяснению логического следования FА1, … , An ⊨ F, что равносильно доказательству:– общезначимости формулы А1 ∧…∧ An → F или– невыполнимости формулы А1 ∧…∧ An ∧ ¬ FПоскольку ИП полуразрешимо:априорное предположение об общезначимости формулы,которое надо доказать метод Эрбрана, 1930 обратный метод Маслова, 1964 метод резолюций Робинсона,1965 –обратный вывод,, практически применимый!21ИСЧИСЛЕНИЕ ПРЕДИКАТОВ:МЕТОД РЕЗОЛЮЦИЙДоказательство выводимости F из аксиом A1 … Anметодом доказательства невыполнимости формулыА1 ∧…∧ An ∧ ¬ F. Все формулы переводятся в конъюнктивную форму ,а кванторы отбрасываются – работа с множеством Mформул-дизъюнкций Обобщенное правило логического вывода: резолюция На каждом шаге вывода из пары дизъюнкций из Mстроится резольвента:B1 ∨ … ∨ P ∨ … ∨ Bk и C1 ∨ … ∨ ¬P ∨ ...∨ Cmих резольвента:B1 ∨ … ∨ Bk ∨ C1 ∨ ...∨ Cm Полученная резольвента добавляется в M Цель – получить пустую резольвенту (тем самымдоказать невыполнимость, т.е.

выводимость F)22МЕТОД РЕЗОЛЮЦИЙ: ДЕТАЛИШаг метода резолюций:1. Выбор из M пары формул, в которых естьконтрарные литералы: предикат Р и его отрицание2. Унификация (обычно – наиболее общая): подстановкавместо переменных выбранных формул определённыхтермов для совпадения всех аргументов Р и ¬Р3. Получение резольвенты и добавление её в MОсобенности: В общем случае неоднозначность: какую пару формулвыбрать? (возможны различные стратегии, перебор) Резольвента может быть длиннее исходных формул,в то время как цель – получить пустую резольвенту В целом: полная система доказательства формул логикипервого порядка для БЗ в конъюнктивной форме23МЕТОД РЕЗОЛЮЦИЙ: ПРИМЕРИсходные утверждения:Кот(Мурзик)х( Кот(х)  Живое_существо(х))у( Живое_существо(у)  Дышит(у))Доказать:Дышит (Мурзик)Множество M :Кот(Мурзик)(1) Кот(х)  Живое_существо(х)(2) Живое_существо(у)  Дышит (у)(3) Дышит(Мурзик)(4)Резольвента (2) и (3): Кот(z)  Дышит(z)(5)Резольвента (4) и (5): Кот(Мурзик)(6)Резольвента (1) и (6): пустая резольвента24ЯЗЫК ПРОЛОГЯзык Пролог – язык предикатов первого порядка, ноособые синтаксис и процедура доказательства.Клаузальная форма записи формул (клаузы Хорна), прикоторой кванторы опускаются, например:пролог-правило P:- Q, R, T.

– это формула Q  R  TP,равносильная ¬Q ¬R ¬T  P – хорновский дизъюнкт,только одно слагаемое без отрицания.Пролог-предложение является хорновским дизъюнктом.Факты и правила Пролога – аксиомы, вопрос – теоремаДышит(у):- Живое_существо(у).Стратегия доказательства – линейная резолюция (SLD)для хорновских дизъюнктов, более эффективнаяПроблемы обратного вывода (от доказываемого факта):незавершаемые и избыточные вычисления25ЯЗЫК DATALOGСинтаксически: подмножество Пролога:ЯП без функциональных символов (функций)DataLog ориентирован на работу с БД: язык запросовОтличающаяся от Пролога семантика: Операции над конечными множествами Порядок предложений не важен: декларативность ! Прямой вывод: доступен для понимания исочетается с реляционными операциями БД Различение экстенсиональных и интенсиональныхпредикатных символов (разделение БЗ) Ограничения на рекурсию, логическое отрицание и др.Важно: разрешимость вывода (полиномиальное время?)Язык запросов: – алгоритмически не полон (по Тьюрингу)– мощнее других языков запросов к БД (рекурсия)26ЗАКЛЮЧЕНИЕИВ и ИП – две формальные системы вывода(дедукции), отражающие общелогическиезаконы, но отличающиеся выразительностью языка.Модельная семантика строится на базенепосредственного установления соответствиясинтаксических понятий языка логики с понятиямиобъектного мира, описываемого этим языком.Формальная логическая система дает возможностьвывода из известных утверждений (знаний) – новыхутверждений (знаний), позволяя более экономнохранить информацию в БЗ.ПЗ в логической модели – на основе прикладной(конкретизированной) формальной теории.27СПАСИБО ЗА ВНИМАНИЕ!28ДОМАШНЕЕ ЗАДАНИЕПовторить основные понятия исинтаксические правила формулисчисления предикатов первогопорядка29.

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

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