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

ПРЕДСТАВЛЕНИЕ ЗНАНИЙ,ЛОГИЧЕСКАЯ МОДЕЛЬ:ФОРМАЛЬНЫЕ ТЕОРИИСОДЕРЖАНИЕ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 , т.