Ещё одни лекции В.А. Захарова

Основыматематическойлогики и логическогопрограммированияЛЕКТОР:Владимир Анатольевич Захаровzakh@cs.msu.suПрограмма курсаhttp://mathcyb.cs.msu.su/courses/logprog.htmlЛекция 1.Что изучает логика?Логика в информатике.Структура курса.Исторические сведения.Логические парадоксы.Что изучает логика?ЛОГИКА — междисциплинарная отрасль наук,изучающаязаконы причинно-следственной связи вокружающем мире;проявление причинно-следственных законов врациональном мышлении человека;отражение причинно-следственных законов вязыках (естественных и искусственных).Что изучает логика?ФОРМАЛЬНАЯ ЛОГИКАизучает формы , в которых проявляются законыпричинно-следственных связей, вне зависимостиот содержания (смысла) тех явлений (предметов),к которым эти законы относятся.Что изучает логика?Поясняющий пример.P1: Каждый металл — проводник.P2: Ртуть — металл.Значит, ртуть — проводник.Закон физики (?)Что изучает логика?Поясняющий пример.P1: В каждом южном городе летом тепло.P2: Сочи — южный город.Значит, в Сочи летом тепло.Закон географии (?)Что изучает логика?Поясняющий пример.P1: Каждый преступник должен бытьнаказан.P2: У.

б. Л. — преступник.Значит, У. б. Л. должен быть наказан.Закон юриспруденции (?)Что изучает логика?Поясняющий пример.Общая форма всех этих законовP1: Каждый предмет, обладающийсвойством R, обладает свойство Q.P2: Предмет c обладает свойством R.Значит, предмет c обладает свойством Q.Закон формальной логики (!!!)Что изучает логика?Поясняющий пример.Общая форма всех этих законовP1: ∀x (R(x) → Q(x)).P2: R(c).Q(c).Закон формальной логики (в символьном виде)Логика в информатикеВернемся к примеру.Это — исходные знания (база знаний).P1: Каждый металл — проводник.P2: Ртуть — металл.А это — новые знания.Ртуть — проводник.Откуда взялись новые знания???Логика в информатикеПрименение закона формальной логики.Логический закон:P1: ∀x (R(x) → Q(x)).P2: R(c).Q(c).Интерпретация:R(x) — «предмет x — металл »;Q(x) — «предмет x — проводник»;c — «ртуть».Логика в информатикеЕще одно применение закона формальной логики.Логический закон:P1: ∀x (R(x) → Q(x)).P2: R(c).Q(c).Другая интерпретация:R(x) — «предмет x — южный город »;Q(x) — «предмет x — теплый летом»;c — «Сочи».Логика в информатикеЛогика не позволяет получать новуюинформацию!!!Знания — это форма представления информации в видеформальных высказываний.Законы формальной логики преобразуют одни высказывания вдругие.Таким образом, законы формальной логики позволяютпреобразовывать информацию из одной формы представленияв другую.Законы формальной логики — этоинструмент преобразования информации.Логика в информатикеОсновная задача формальной логики.База знаний: Γ = {ϕ1 , ϕ2 , .

. . , ϕN }.Предложение: ψ.Задача (неформальная): выяснить, является липредложение ψ следствием утверждений базы знаний Γ.Задача (формальная): проверить, что ψ выводится из Γ позаконам формальной логики.Логика в информатикеПриложение 1.Экспертные системы.База знаний Γ — база знаний экспертной системы.Предложение ψ — запрос к базе знаний.Аппарат логического вывода — ядро экспертной системы.Приложение 2.Автоматизация научных исследований.База знаний Γ — система аксиом математической теории.Предложение ψ — математическое утверждение.Аппарат логического вывода — ядро автоматическойсистемы доказательства теорем.Логика в информатикеПриложения 1, 2.Для этого нужно уметь:Разработать формальный язык для представления знаний.Создать систему необходимых законов формальнойлогики.Проверить корректность логических законов.Проверить полноту построенной системы логическихзаконов.Разработать алгоритм проверки выводимости однихпредложений из других по заданным законам.Этим мы займемся в первой части курса.Оптимизировать построенный алгоритм (сделать егопрактически пригодным).Этим мы займемся во второй части курса.Логика в информатикеПриложение 3.Программирование.Вычисление программы — последовательное преобразованиеинтерпретатором одних состояний данных в другие согласнозаданному алгоритму .Логический вывод (доказательство) — последовательноепостроение по законам формальной логики одних утвержденийиз других, исходя из заданной базы знаний .База знаний Γ — программа.Предложение ψ — вызов программы.Аппарат логического вывода — интерпретатор программ.Но вычисление программы завершается результатом, однако,не всякое доказательство является «результативным»(конструктивным).Логика в информатикеПриложение 3.Пример.Задача.

Существуют ли такие два иррациональных числа α иβ, что αβ — рациональное число?Решение. √√√ 21. Если 2 — рациональное число, то α = β = 2.√ √22. Если 2√ — иррациональное число, то√√ 2α = 2 , β = 2.Мы доказали, что α и β существуют, но не смогли ихвычислить. Это неконструктивное доказательство.Чтобы логическое доказательство могло играть рольвычисления, оно должно быть конструктивным.Логика в информатикеПриложение 3.Для этого нужно уметь:Разработать формальный язык для представленияпрограмм в виде логических утверждений.Сделать логическое доказательство конструктивным,чтобы оно могло играть роль вычисления.Проверить вычислительную корректность этого способадоказательства.Проверить алгоритмическую полноту этого способадоказательства.Сделать этот способ программирования удобным дляпользования.Этим мы займемся в третьей части курса.Логика в информатикеПриложение 4.Программы могут быть правильными и неправильными.Правильная программа — это такая программа, поведениекоторой удовлетворяет заданным требованиям (спецификации)корректности.Проверить правильность программы — значит доказать, чтопрограмма удовлетворяет требованиям корректности.Для доказательства правильности программ могут бытьиспользованы методы логики.Логика в информатикеПриложение 4.Для этого нужно уметь:Разработать формальный язык для описания требованийправильности программ.Разработать правила логического доказательстваправильности программ.Разработать алгоритм (метод) применения этих правилдля доказательства правильности программ относительнозаданных спецификаций.Этим мы займемся в четвертой части курса.Исторические сведения384 д.н.э.322 д.н.э.АРИСТОТЕЛЬИсторические сведения16461716ГОТФРИД ВИЛЬГЕЛЬМ ФОН ЛЕЙБНИЦИсторические сведения18151864ДЖОРДЖ БУЛЬИсторические сведения18481925ГОТТЛОБ ФРЕГЕИсторические сведения18621943ДАВИД ГИЛЬБЕРТИсторические сведения18721970БЕРТРАН РАССЕЛИсторические сведения19061978КУРТ ГЕДЕЛЬИсторические сведения19021983АЛЬФРЕД ТАРСКИЙИсторические сведения19081931ЖАК ЭРБРАНИсторические сведения19091945ГЕРХАРД ГЕНЦЕНИсторические сведения1941АЛАН КОЛМЕРОЭИсторические сведения1956МИХАИЛ ЗАХАРЬЯЩЕВЛогические парадоксы.Парадоксы - движущая сила логики.Противоречивые парадоксы (антиномии ) заставляютзадумываться над такими вопросами, какЧто такое истинное утверждение?Что такое доказуемое утверждение?В какой мере можно формализовать наши знания?Логические парадоксы.Парадокс о крокодилеКрокодил схватил ребенка.Мать ребенка просит крокодила:«Верни мне ребенка! »Крокодил отвечает:«Я верну тебе ребенка, если тыугадаешь, исполню ли я твою просьбу.

»«Не исполнишь », — говорит женщина.Вернет ли крокодил ребенка матери?Логические парадоксы.Парадокс лжецаУТВЕРЖДЕНИЕ,КОТОРОЕ НАПИСАНО НАЭТОМСЛАЙДЕ, — ЛОЖНОЕ.Логические парадоксы.Парадокс лжецаИстинно или ложно предъявленное вамутверждение?Логические парадоксы.Парадокс утренней звездыВенера видна ранним вечером, и поэтомуее называют вечерней звездой.Венера видна ранним утром, и поэтомуее называют утренней звездой.Означает ли это, что вечерняя звездавидна ранним утром?Логические парадоксы.Парадокс морской битвыНекий флотоводец обратился к прорицателю с вопросом,состоится ли завтра морская битва. Прорицатель ответил:«Битва завтра состоится».На следующий день случился шторм, и флот не смог выйти вморе.

Разгневанный флотоводец потребовал от прорицателявернуть деньги, поскольку его прогноз оказался ложным.Прорицатель ответил:«Твои моряки вчера купили на рынкесвежее молоко. Сегодня это молоко уже не свежее, но они непросят вернуть им деньги обратно. Мой прогноз тоже былверным вчера, и ты не вправе жаловаться на то, что он неверенсегодня».Прав ли прорицатель?Парадоксы неизбежны.Но их влияние можно ограничить.Для этого нужны математические моделилогических законов.Так появиласьМатематическая логикаРЕЙМОНД С.

СМАЛЛИАН. "Как же называется эта книга?"У Порции (героини комедии "Венецианский купец") было тришкатулки: из золота, серебра и свинца. В одной из шкатулокхранился портрет Порции. Поклоннику предлагалось выбратьшкатулку, и если он был достаточно умен, чтобы выбратьшкатулку с портретом, то получал право назвать Порциюневестой. На крышках шкатулок были надписи:На золотойПортрет в этойшкатулкеНа серебрянойПортрет не в этойшкатулкеНа свинцовойПортрет не в золотойшкатулкеСвоему поклоннику Порция пояснила, что из трехвысказываний на крышках шкатулок, по крайней мере дваложны.Какую шкатулку следует выбрать поклоннику Порции?КОНЕЦ ЛЕКЦИИ 1.Основыматематическойлогики и логическогопрограммированияЛЕКТОР:Владимир Анатольевич Захаровzakh@cs.msu.suhttp://mathcyb.cs.msu.su/courses/logprog.htmlЛекция 2.Классическая логика предикатовпервого порядкаСинтаксис.

Термы и формулы.Семантика. Интерпретация.Выполнимость формул.ПРЕДИКАТлатинский термин («предвидеть,предсказывать»), обозначающийчлен предложения — сказуемое.CтудентCубъектслушаетПредикатлектораОбъектВ более общем смысле предикат — этосвойство, атрибут предмета, отношениемежду предметами, событиями,явлениями.АЛФАВИТБазовые символы.Предметные переменныеVar = {x1 , x2 , . . . , xk , . . . };Предметные константыConst = {c1 , c2 , .

. . , cl , . . . };Функциональные символыFunc = {f1Предикатные символыPred = {P1(n1 )(n2 ), f2(m1 )(m2 ), P2(nr ), . . . , fr, . . . };(ms ), . . . , PsТройка Const, Pred, Func называется сигнатурой алфавита., . . . }.АЛФАВИТБазовые символы.Предметные константы— это имена предметов;Функциональные символыобозначают операциинад предметами;Предикатные символыобозначают отношениямежду предметами.Пример.Константы0, 1, π, . . . ;Функциональные символы+, ×,mod , .

. . ;Предикатные символы=, <, . . . .АЛФАВИТЛогические связки и кванторы.КонъюнкцияДизъюнкцияОтрицаниеИмпликация(логическое(логическое(логическое(логическоеКвантор всеобщностиКвантор существованияЗнаки препинания.РазделительСкобки,()И)ИЛИ)НЕ)ЕСЛИ-ТО)&∨¬→.(«для каждого»)(«хотя бы один»)∀∃СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫОпределение терма.Терм — этоxcf (n) (t1 , t2 , . . . , tn ), если x ∈ Var, если c ∈ Const, если f (n) ∈ Funct1 , t2 , . . . , tn — термыx — переменная;c — константа;составной терм.Term — множество термов заданного алфавита.Vart — множество переменных, входящих в состав терма t.t(x1 , x2 , .