Теормин 2014 (avasite) (1158133)

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

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

Лекция 1. Что изучает логика. Логика в информатике. Структура курса...

ЛОГИКА — междисциплинарная отрасль наук, изучающая

1. законы причинно-следственной связи в окружающем мире;

2. проявление причинно-следственных законов в рациональном мышлении человека;

3. отражение причинно-следственных законов в языках (естественных и искусственных).

ФОРМАЛЬНАЯ ЛОГИКА – изучает формы, в которых проявляются законы причинно-следственных связей, вне зависимости от содержания (смысла) тех явлений (предметов), к которым эти законы относятся.

Основная задача формальной логики:

База знаний: Γ = {ϕ₁, ϕ₂, …, ϕ_N}.

Предложение: ψ.

Задача (неформальная): выяснить, является ли предложение ψ следствием утверждений базы знаний Γ.

Задача (формальная): проверить, что ψ выводится из Γ по законам формальной логики.

Лекция 2. Классическая логика предикатов первого порядка. Синтаксис. Термы и формулы. Семантика. Интерпретация. Выполнимость формул.

Базовые символы.

Предметные переменные Var = {x1, x2, . . . , xk, . . . };

Предметные константы Const = {c1, c2, . . . , cl, . . . } – это имена предметов

Функциональные символы Func = {f(n1)1, f(n2)2, . . . , f(nr )r, . . . } – это операции над предметами

Предикатные символы Pred = {P(m1)1, P(m2)2, . . . , P(ms )s , . . . } – это отношения между предметами.

Тройка <Const , Pred , Func> называется сигнатурой алфавита.

Терм — это

1. x , если x ∈ Var (x — переменная)

2. c , если c ∈ Const (c — константа)

3. f⁽ⁿ⁾(t1, t2, . . . , tn) , если f(n)∈ Func и (t1, t2, . . . , tn — термы) – составной терм.

Term — множество термов заданного алфавита.

Var t— множество переменных, входящих в состав терма t.

t (x1, x2, . . . , xn) — запись обозначающая терм t , у которого Var t⊆ {x1, x2, . . . , xn}.

Если Vart = ∅, то терм t называется основным термом.

Формула — это атомарная формула P(m)(t1, t2, . . . , tm) , если P(m)∈ Pred , {t1, t2, . . . , tm} ⊆ Term;

составная формула:

(ϕ&ψ), (ϕ ∨ ψ), (ϕ → ψ), (¬ϕ), если ϕ, ψ — формулы;

(∃x ϕ), (∀x ϕ) , если x ∈ Var , ϕ — формула.

Form — множество всех формул заданного алфавита.

Свободные и связанные переменные.

Квантор связывает ту переменную, которая следует за ним. Вхождение переменной в области действия квантора,

связывающего эту переменную, называется связанным. Вхождение переменной в формулу, не являющееся связанным, называется свободным. Переменная называется свободной, если она имеет свободное вхождение в формулу.

Var ϕ — множество свободных переменных формулы ϕ.

ϕ(x1, x2, . . . , xn) — запись, обозначающая формулу ϕ, у которой Var ϕ⊆ {x1, x2, . . . , xn}.

Если Varϕ = ∅, то формула ϕ называется замкнутой формулой, или предложением.

CForm — множество всех замкнутых формул.

Приоритет логических операций:

¬, ∀, ∃ & ∨ →

Семантика — это свод правил, наделяющих значением (смыслом) синтаксические конструкции языка.

Значения термов и формул определяются на основе алгебраических систем.

Алгебраические системы, используемые в таком качестве, называются интерпретациями.

Интерпретация сигнатуры <Const, Func, Pred> — это алгебраическая система I = <DI, Const, Func, Pred>, где

1. DI— непустое множество, которое называется областью интерпретации, предметной областью, или универсумом

2. Const (с чертой сверху): Const → DI — оценка констант, сопоставляющая каждой константе c элемент (предмет) c (с чертой сверху) из области интерпретации;

3. Func: Func(n) → (DnI → DI) — оценка функциональных символов, сопоставляющая каждому функциональному символу f(n) местности n всюду определенную n-местную функцию f(n) на области интерпретации;

4. Pred : Pred(m) → (DmI → {true, false}) — оценка предикатных символов, сопоставляющая каждому предикатному символу P(m) местности m всюду определенное m-местное отношение P(m) на области интерпретации.

Значение терма

Пусть заданы интерпретация I = <DI, Const, Func, Pred>, терм t(x1, x2, . . . , xn) и набор d1, d2, . . . , dn элементов (предметов) из области интерпретации DI.

Значение t(x1, x2, . . . , xn)[d1, d2, . . . , dn] терма t (x1, x2, . . . , xn)на наборе d1, d2, . . . , dn определяется рекурсивно

1. Если t (x1, x2, . . . , xn) = xi, то t(x1, x2, . . . , xn)[d1, d2, . . . , dn] = di

2. Если t (x1, x2, . . . , xn) = c, то t(x1, x2, . . . , xn)[d1, d2, . . . , dn] = c(с чертой сверху)

3. Если t (x1, x2, . . . , xn) = f(t1, . . . , tk), то t(x1, x2, . . . , xn)[d1, d2, . . . , dn] = f(t1[d1, d2, . . . , dn], . . . , tk[d1, d2, . . . , dn]) (с чертой сверху)

Отношение выполнимости формул

Значение формул в интерпретации определяется при помощи отношения выполнимости |=. Пусть заданы интерпретация I = <DI, Const, Func, Pred>, формула ϕ(x1, x2, . . . , xn) и набор d1, d2, . . . , dn элементов (предметов) из области интерпретации DI.

Отношение выполнимости I |= ϕ(x1, x2, . . . , xn)[d1, d2, . . . , dn], формулы ϕ в интерпретации I на наборе d1, d2, . . ., dn определяется рекурсивно – Если ϕ(x1, x2, . . . , xn) = P(t1, . . . , tm), то I |= ϕ(x1, x2, . . . , xn)[d1, d2, . . . , dn] ⇐⇒ P(t1[d1, d2, . . . , dn], . . . , tm[d1, d2, . . . , dn]) (с чертой сверху) = true

Лекция 3. Выполнимые и общезначимые формулы. Модели. Логическое следование. Проблема общезначимости. Семантические таблицы.

Формула ϕ(x1, . . . , xn) называется выполнимой в интерпретации I, если существует такой набор элементов d1, . . . , dn ∈ DI, для которого имеет место I |= ϕ(x1, . . . , xn)[d1, . . . , dn].

Формула ϕ(x1, . . . , xn) называется истинной в интерпретации I, если для любого набора элементов d1, . . . , dn ∈ DI имеет место I |= ϕ(x1, . . . , xn)[d1, . . . , dn].

Формула ϕ(x1, . . . , xn) называется выполнимой, если есть интерпретация I, в которой эта формула выполнима.

Формула ϕ(x1, . . . , xn) называется общезначимой (или тождественно истинной), если эта формула истинна в любой интерпретации.

Формула ϕ(x1, . . . , xn) называется противоречивой (или невыполнимой), если она не является выполнимой.

Пусть Γ — некоторое множество замкнутых формул, Γ ⊆ CForm. Тогда каждая интерпретация I, в которой выполняются все формулы множества Γ, называется моделью для множества Γ.

Модель для множества формул Γ — это интерпретация (реальный или виртуальный мир), устройство которого адекватно всем предложениям из множества Γ.

Пусть Γ — некоторое множество замкнутых формул, и ϕ — замкнутая формула. Формула ϕ называется логическим следствием множества предложений (базы знаний) Γ, если каждая модель для множества формул Γ является моделью для формулы ϕ,

т. е. для любой интерпретации I : I |= Γ ⇒ I |= ϕ

Логические следствия — это «производные» знания, которые неизбежно сопутствуют «базовым» знаниям Γ, находятся в причинно-следственной зависимости от предложений Γ. Одна из главных задач (и одновременно наиболее характерное проявление) интеллектуальной деятельности — это извлечение логических следствий из баз знаний.

Запись Γ |= ϕ обозначает, что ϕ — логическое следствие Γ .

Поэтому для обозначения общезначимости формулы ϕ будем использовать запись |= ϕ.

Теорема о логическом следствии

Пусть Γ = {ψ1, . . . , ψn} ⊆ CForm, ϕ ∈ CForm. Тогда Γ |= ϕ ⇐⇒ |= (ψ1& . . . &ψn → ϕ).

(доказательство – по определениям)

Утверждение.

Для любой формулы ϕ(x1, . . . , xn) верно, что

1. |= ϕ(x1, . . . , xn) ⇐⇒ |= ∀x1. . . ∀xn ϕ(x1, . . . , xn);

2. ϕ(x1, . . . , xn) — выполнимая ⇐⇒ ∃x1. . . ∃xn ϕ(x1, . . . , xn) — выполнимая;

3. ϕ(x1, . . . , xn) — выполнима в любой интерпретации ⇐⇒ |= ∃x1. . . ∃xn ϕ(x1, . . . , xn).

Утверждение.

Существует такая замкнутая формула ϕ, которая истинна в любой интерпретации I с конечной предметной областью DI, но не является общезначимой.

(из свойства иррефлексивности и транзитивности -> «свойство максимального элемента», доказательство не строгое – через аналогию с начальником, который командует подчинённым (одно число больше другого))

Семантическая таблица — это упорядоченная пара множеств формул <Γ ; ∆>, Γ, ∆ ⊆ Form.

Γ — это множество формул, которые мы хотим считать истинными, ∆ — это множество формул, которые мы хотим считать ложными.

Пусть {x1, x2, . . . , xn} — множество свободных переменных в формулах множеств Γ, ∆.

Семантическая таблица <Γ ; ∆> называется выполнимой, если существует такая интерпретация I и такой набор значений d1, d2, . . . , dn ∈ DI свободных переменных, для которых

1. I |= ϕ(x1, x2, . . . , xn)[d1, d2, . . . , dn] для любой формулы ϕ, ϕ ∈ Γ

2. I |≠ ψ(x1, x2, . . . , xn)[d1, d2, . . . , dn] для любой формулы ψ, ψ ∈ ∆.

Теорема (о табличной проверке общезначимости)

|= ϕ ⇐⇒ таблица Tϕ = <∅ ; {ϕ}> невыполнима.

(доказательство по определению)

Закрытая семантическая таблица. Семантическая таблица <Γ ; ∆>, у которой Γ ∩ ∆ ≠ ∅, называется закрытой.

Утверждение

Закрытая таблица невыполнима.

Атомарная семантическая таблица. Семантическая таблица <Γ; ∆>, у которой множества Γ, ∆ состоят только из атомарных формул, называется атомарной.

Утверждение

Незакрытая атомарная таблица выполнима.

Доказательства такого вида (через преобразование таблицы Tϕ = <∅; {ϕ}> к закрытой) называются логическим выводом.

Если в выводе участвуют семантические таблицы, то логический вывод называется табличным семантическим выводом.

Подстановка – это всякое отображение θ: Var → Term, сопоставляющее каждой переменной некоторый терм.

Множество Dom_θ = {x : θ(x) ≠ x} называется областью подстановки. Если область подстановки – это конечное множество переменных, то такая подстановка называется конечной. Множество конечных подстановок обозначим Subst.

Если θ ∈ Subst и Dom_θ = {x1, x2, …, xn}, то подстановка θ однозначно определяется множеством пар {x1/θ(x1), x2=θ(x2), …, xn=θ(xn)}.

Каждая пара xi=θ(xi) называется связкой.

Для заданного логического выражения E и подстановки θ запись Eθ обозначает результат применения подстановки к E который определяется так:

Если E = x, x ∈ Var, то Eθ = (x)

Если E = c, c ∈ Const, то Eθ = c

Если E = f(t1, t2, …, tk), то Eθ = f(t1θ, t2θ, …, tnθ)

Если E = P(t1, t2, …, tk), то Eθ = P(t1θ, t2θ, …, tnθ)

Если E = φ&Ψ, то E = φ&Ψ (аналогично для формул φ→Ψ, φvΨ, ¬φ)

Если E = ∀x0 φ, то Eθ = ∀x0(φθ’), где η – новая подстановка, удовлетворяющая условию. Θ’(x) = { x0, если x = x0; θ(x), если x ≠ x0} (аналогично для формул ∃x0 φ).

Переменная x называется свободной для терма t в формуле φ(x), если любое свободное вхождение переменной x в формуле φ(x), не лежит в области действия ни одного квантора, связывающего переменную из множества Var t.

Подстановка θ = {x1/t1, …, xn/tn}, называется правильной для формулы φ, если для любой связки xi/ti переменная xi свободна для терма ti в формуле φ.

Лекция 4. Подстановки. Табличный вывод. Корректность табличного вывода.

Здесь должна быть лекция 4, но из-за лагов с кодировкой у меня ничего не вышло, так что сокращённый вариант – т.е. без формулировок

Подстановка

Область подстановки

Результат применения подстановки

Переменная, свободная для терма

Подстановка, правильная для формулы

Табличный вывод – это корневое дерево, в котором корнем является сама таблица, дуги выходят в соответствии с правилами табличного вывода, а листьями служат либо закрытые таблицы, либо атомарные таблицы

Успешный табличный вывод – если дерево вывода – конечно и все его листья – закрытые таблицы

Лемма о корректности правил вывода

Каково бы ни было правило табличного вывода, исходная таблица выполнима <=> выполнима таблица, порождённая правилом (одна или обе, если их 2)

(доказательство по определению, для существования доказывается построением новой интерпретации, отличающейся от изначальной (в которой верна первая таблица) лишь равенством константы – подставленному объекту интерпретации)

Теорема корректности табличного вывода

Если для таблицы существует успешный табличный вывод, то она невыполнима

(следует из определения, леммы о корректности правил и утверждения о невыполнимости закрытых таблиц)

Следствие

Если для таблицы T=<∅|ϕ> можно построить успешный табличный вывод, то |= ϕ

Лекция 5. Полнота табличного вывода. Теорема Левенгейма-Сколема. Теорема компактности Мальцева. Автоматическое доказательство теорем.

Теорема полноты табличного вывода

Если семантическая таблица T0 невыполнима, то для T0 существует успешный табличный вывод.

(Доказательство конструктивно, в нём указывается, как нужно использовать табличный вывод (Лекция 5 Слайд 3-36) (do not be afraid of the number of pages))

(Доказательство проводится для упрощённой задачи – для конечного числа формул, все они замкнуты и в них нет функциональных символов. Суть в том, что мы последовательно раскрываем вширь дерево табличного вывода нумеруя таблицы, в таблице – упорядоченные списки формул, и с ней ассоциировано множество уже использованных констант. Далее от обратного – пусть нет успешного табличного вывода, тогда либо он бесконечен, либо есть атомарная незакрытая таблица (противоречие очевидно), если бесконечная, то постоим множество объединений всех формул, которые входят в эту цепь и констант, для них есть интерпретация в которой всё это выполнено, потом индуктивно по количеству логических операций доказываем, что любая формула из множества составленного из выполнимой части таблицы будет выполнима в выбранной интерпретации, и из другой части таблицы – невыполнима, а значит таблица выполнима в этой интерпретации – противоречие условию)

(Несмотря на полное указание алгоритма, на основе которого можно строить пруверы, есть всё ещё проблема с тем, что порой очень много проблем с перебором, и для его уменьшения извращаются по-разному, но этот вопрос всегда открыт)

Теорема Геделя (о полноте)

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

Тип файла документ

Документы такого типа открываются такими программами, как Microsoft Office Word на компьютерах Windows, Apple Pages на компьютерах Mac, Open Office - бесплатная альтернатива на различных платформах, в том числе Linux. Наиболее простым и современным решением будут Google документы, так как открываются онлайн без скачивания прямо в браузере на любой платформе. Существуют российские качественные аналоги, например от Яндекса.

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

Файлы такого типа обычно разбиты на страницы, а текст может быть форматированным (жирный, курсив, выбор шрифта, таблицы и т.п.), а также в него можно добавлять изображения. Формат идеально подходит для рефератов, докладов и РПЗ курсовых проектов, которые необходимо распечатать. Кстати перед печатью также сохраняйте файл в PDF, так как принтер может начудить со шрифтами.

Список файлов ответов (шпаргалок)