МПЗиО_2_17_ЛогичТеории (1185821)

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

Текст из файла

ПРЕДСТАВЛЕНИЕ ЗНАНИЙ,ЛОГИЧЕСКАЯ МОДЕЛЬ:ФОРМАЛЬНЫЕ ТЕОРИИСОДЕРЖАНИЕ1. Логическая модель ПЗ : sinopsis2. Понятие формальной/логической теории компоненты, семантика, свойства3. Исчисление высказываний (ИВ) язык, интерпретации, свойства4. Исчисление предикатов первого порядка (ИП) язык предикатов, семантика, свойства5. Доказательство теорем: метод резолюций6. Языки Prolog и Datalog7. Заключение, Домашнее задание2ЛОГИЧЕСКАЯ МОДЕЛЬИсторически первая: применение для ПЗуже существующего языка предикатов (ЯП) ЯП разработан ходе исследования логическихоснов ЕЯВ логической модели знания представляются каксовокупность правильных формул какой-либоформальной логической системыДостоинства формальных логических систем: изученность свойств возможность применения механизмаформального вывода (доказательства)Операции над знаниями – на основе логическоговывода3ФОРМАЛЬНАЯ СИСТЕМАФормальная логическая система/логика/теория Истоки появления: изучение и формализацияИстинность Vs.

ДоказуемостьИдея замены доказательства/рассуждения – вычислением,формальными символьными преобразованиями строк Формализация, аксиоматизация математических теорий,теоремы – формулы, выводимые из формул-аксиомФормальные логические теории отличаются повыразительной мощности и эффективности выводаИсчисление (логика) высказыванийИсчисление (логика) предикатов первого порядкаМногосортные логики первого порядкаДескриптивные логикиМодальные логики (возможность/необходимость)Нечеткая и вероятностная логики4ФОРМАЛЬНАЯ СИСТЕМА:КОМПОНЕНТЫФормальная логическая система / логика / теориязадается четверкой компонент: T = < E, R, A, P > E – множество базовых элементов формул R – синтаксические правила, на основе которых изэлементов Е образуются синтаксически правильные(правильно построенные) формулы теории A – множество аксиом: подмножество всего множествасинтаксически правильных формул, которым априорноприписывается статус истинности. P – множество правил формального вывода(оперирования символами), применяя которыек формулам (аксиомам), можно получать новые п.п.формулы (теоремы):F Ⱶ G (G выводима из F)E+R – сигнатура теории (ее язык)5ФОРМАЛЬНАЯ СИСТЕМА:ИНТЕРПРЕТАЦИЯИнтерпретация I, или формальная семантика: Задаются: Область интерпретации D иФункция, сопоставляющая каждой формуле F теориинекоторое содержательное высказывание P (истинноеили ложное) относительно объектов множества D Формула F:Выполнима, если существует интерпретация, где P истинноОбщезначима, если истинна в любой интерпретацииПротиворечива (невыполнима), если ложна в любойинтерпретацииЛогическое следствие: F ⊨ G, если G выполнима(истинна) в любой интерпретации, в которой выполнима FФормальная семантика называется также модельной:модель теории T – интерпретация, в которой ни однатеорема не является противоречивой (все выполнимы)6ФОРМАЛЬНАЯ СИСТЕМА:ОСНОВНЫЕ СВОЙСТВАДля формальной теории T : Полнота (содержательная, относительно интерпретации):Любому истинному высказыванию P соответствуеттеорема в T (т.е.

истинность P м.б. обоснована выводом) НепротиворечивостьФормальная: не выводимы одновременно формулы F и ¬FСодержательная: существует модельРазрешимость: существует алгоритм, который для любойформулы F определяет, является ли она теоремой(истинность/ложность формулы)Полуразрешимость: существует алгоритм, который длялюбой формулы-теоремы дает положительный ответ(для нетеорем алгоритм может зациклиться)Вычислительная сложность – важный вопрос7ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ Элементы логических рассуждений – простыевысказывания (истинные или ложные)МГУ основано в 1755 году Пропозиция (proposio) – предложение/высказывание,рассматриваемое только с точки зрения истинностиE – пропозициональные переменные: p, q, r, …логические связки: ¬ (отрицание), → (импликация)логические значения (истина и ложь): ⊤ и ⊥служебные символы: скобки и запятыеR – индуктивные правила:п.п.формула –1) переменная 2) логическое значение3) ¬ F ; F1 → F2 , где F, F1, F2 – п.п.формулыДругие логические связки вводятся как синтаксическиесокращения:x  y ≡ ¬ (x → ¬ y) x  y ≡ ¬ x→ yПример п.п.формулы:¬ q  (p → ¬ r)8ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ:ИНТЕРПРЕТАЦИЯТрадиционная:Булева алгебра(или алгебра высказываний, алгебра булевских функций)Каждой пропозициональной переменной ставится всоответствие истинностное значение (истина/ложь – 1 / 0)Логические связки трактуются традиционно, каксоответствующие булевские функцииТогда любая п.п.

формула получает истинностноезначениеВ такой интерпретации:p → ¬ p выполнимаp  ¬ p общезначима;p  ¬ p противоречиваДля Булевой алгебры есть процедура (алгоритм)определения для любой формулы-функции всех еезначений (построение таблицы истинности)9ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ:ЛОГИЧЕСКИЙ ВЫВОДАксиомы и правила вывода ИВ? –дедуктивная система (A + P)Возможно несколько аксиоматизаций, например,КИВ (классическое исчисление высказываний):A – 3 аксиомы, в том числе (А →(В → А))P – правило отделения (modus ponens): А , А → ВПример теоремы:ВͰ (¬ q → ¬ p) → (p →q)Теоремы (законы) ИВ – схемы истинных сложныхвысказываний (утверждений):Ͱ (¬ q → ¬ p) → (p →q)Ͱ (¬ p → (q  ¬ q)) → p10ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ:СВОЙСТВА ТЕОРИИОсновные свойства ИВ : Полнота: теоремы и только они являютсяобщезначимыми формулами Непротиворечивость (оба вида) Разрешимость Стандартная разрешающая процедура проверкиобщезначимости формулы (по таблице истинности) Алгоритм DPLL проверки выполнимости формул ИВв конъюнктивной нормальной форме (NP-полнаязадача: правило резолюции + поиск с возвратами)Эффективность вывода, однако :Язык (сигнатура) ИВ – слабая выразительность11ИСЧИСЛЕНИЕ ВЫСКАЗЫВАНИЙ:ДРУГАЯ ИНТЕРПРЕТАЦИЯСемантика множеств (предикатная семантика) Область интерпретации D ; пропозицион.

переменным(высказываниям) ставятся в соответствие подмножества DИнтерпретация логических связок и значений:⊤–D;⊥ – Ø;¬F – D\F;A∨B – A B(F, A, B – формулы)A∧B – A BA → B – A  B : вложение мн-в, A влечет B (“если A то B”)Доказана эквивалентность двух семантик (свойств), т.о.ИВ описывает не только законы логических операций надпростыми высказываниями, но и законы, которымподчиняются операции над множествамиТрадиционную булевскую семантику можно рассматриватькак одноэлементную интерпретацию12ИСЧИСЛЕНИЕ ПРЕДИКАТОВСущественно бóльшая выразительность: Элементы логических рассуждений –высказывательные формы, зависящие от переменных:Он живет в городе Нижний Новгород Входящие в формы объекты могут задаваться не толькоименами, но и более сложным способом:именные формы, зависящие от переменных и констант:sin(x) > 0.5Том любит свою сестру Сложный способ именования объектов задается в ИПпонятием терма:сестра (Том) Высказывательная форма – это предикат (если нетпеременных, вырождается в простое высказывание) Роль формул ИП – описывать сложные высказывания,состоящие из предикатов, к которым могут бытьприменены операторы существования и общности13ИСЧИСЛЕНИЕ ПРЕДИКАТОВ:ЭЛЕМЕНТЫ ФОРМУЛМножество E базовых элементов формул включает: E1 – предметные постоянные/константы a, b, c, …E2 – множество функциональных символов f, g, h,…E3 – множество предикатных символов P, Q, R, ....E1  E2  E3 называется обычно сигнатурой теорииВспомогательные символы: E4 – множество предметных переменных x, y, z, … E5 – логические связки ∧ , ∨ , ¬ , →икванторы: ∀ (всеобщность) и ∃ (существование) E6 – служебные символы: запятые, скобкиДля каждого функционального и предикатного символаопределена арность (число аргументов): n ≥ 0(при n=0 вырождаются в константы и пропозиц.

переменные)14ИСЧИСЛЕНИЕ ПРЕДИКАТОВ:СИНТАКСИЧЕСКИЕ ПРАВИЛАТерм – это либо предметная переменная предметная постоянная/константа выражение вида f(t1,…tn) , где f – функц. символ,а t1,…tn – термыЭлементарная (атомарная) формула – это выражение видаP(t1,…tk) , где P – предикатный символ, а t1,…tk – термыФормула (п.п. формула) – это либо элементарная формула выражение  F, F → G, ∀ x (F) , ∃ x (F) , где F и G – п.п.ф.Теория первого порядка: кванторы могут связывать только предм. переменные,запрещены кванторы по предикатам и функц. символам предикаты не могут быть аргументами др. предикатов15ИСЧИСЛЕНИЕ ПРЕДИКАТОВ:ПРИМЕРЫ ФОРМУЛ x (Р(x) ∨  Р(x))(2) x  y Q(x,y) →  y  x Q(x,y) x (Студент(x) ∧ Старший(курс(x)) →(3) y Научный_руководитель(y, x))(1)Термы содержательно интерпретируются как именаобъектов/сущностейДизъюнкция и конъюнкция вводятся как синтаксическиесокращенияСкобки указывают порядок операций и область действиякванторов, их можно опускать с учетом установленногоприоритета:, ,,∧,∨,→Формула замкнута, если в ней нет свободных (т.е.

несвязанных кванторами) переменных – см. примеры 1-316ИСЧИСЛЕНИЕ ПРЕДИКАТОВ:ЧИСТОЕ И ПРИКЛАДНОЕДедуктивная система (Аксиомы и правила вывода) ?Один из вариантов: A – 3 аксиомы КИВ + 2 аксиомы: универсальнаяконкретизация и экзистенциональное обобщение P – правило отделения (modus ponens)+ 2 правиласвязывания квантором общности и существованияЧистое ИП – в нем нет предметных констант, функций,собственных (дополнит.) аксиом (слайд 15, примеры 1, 2)Выражает «чистую» логику (сугубо логические законы)Прикладное ИП – в сигнатуре есть постоянные и функции(слайд 15, пример 3 , а также:формальная арифметика, теория равенства и др.)Вложение теорий:ИВ  ЧистИП  ПриклИП17ИСЧИСЛЕНИЕ ПРЕДИКАТОВ:ИНТЕРПРЕТАЦИЯИнтерпретация I прикладного ИП на области D : Каждой предметной постоянной ставится в соответствиеэлемент из D Каждому функциональному n-местному символу –функция (операция) f :D n → D Каждому n-местному предикатному символу –отношение R на множестве D Логические связки трактуются традиционно (бул.

функции) Кванторы для одноместных предикатов : x Р(x) = ∧ Р(ci )ci D (бескон. мн-во формул) x Р(x) = ∨ Р(ci )ci  DДля многоместных предикатов – аналогично.Так получается содержательное высказывание на D ,и всякая замкнутая формула истинна /ложна в заданной I18ИСЧИСЛЕНИЕ ПРЕДИКАТОВ:ПОЛНОТАОбщезначимость/Выполнимость/Непротиворечивостьформул: x (Р(x) ∨  Р(x)) ? x  y Q(x,y) →  y  x Q(x,y)?(Замечание: незамкнутая формула истинна винтерпретации I , т.

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

Тип файла PDF

PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

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