Теормин 2014 (avasite)

Лекция 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))

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

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

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