Теормин (Кунцьо)

created by : Кунцьо Степан aka StepLg (421)version/date : 0.3 / 14.11.2008thanks to : Азимов Александр aka mitradir (421) за доскональную проверкуmailto : StepLg@GMail.comhomepage : http://github.com/StepLg/book-mathlog-theormin— термин, обозначающий член предложения — сказуемое.предикат — отношение между лицами, предметами, событиями, явлениями.логика предикатов — изучает законы причинно-следственной зависимости между событиями, представленными в виде отношений.Язык логики предикатов определяетсяпредикат•••алфавитом,синтаксисом,семантикойБазовые символы••••предметные переменные (Var) — имена предметовпредметные константы (Const) —функциональные символы (Func) — операции над предметамипредикатные символы (Pred) — отношения между предметамиСигнатура алфавита - тройка < Const, Pred, Func >Логические связки и кванторы••••••конъюнкциядизъюнкцияотрицаниеимпликацияквантор всеобщностиквантор существованияЗнаки препинания: разделитель запятая и скобкиТермы — предметы, вступающие в отношения друг с другом.Терм — рекурсивное определение (2.8)Term — множество термов заданного алфавитаV art — множество переменных, входящих в состав заданного терма t1— такой терм t, что его V art = ∅Формула — рекурсивное определение (2.10) через атомарнуюОсновной термформулуформулуи составнуюForm — множество всех формул заданного алфавитаКвантор связывает ту переменную, которая следует за ним.Связанное вхождение переменной — вхождение этой переменной в области действияквантора, связывающего ее.Свободное вхождение переменной — вхождение, не являющееся связанным.Свободная переменная — переменная, имеющая свободное вхождение в формулу.V arϕ — множество всех свободных переменных формулы ϕ.Замкнутая формула (предложение) — такая формула, у которой V arϕ = ∅.Приоритеты логических операций: {¬, ∃, ∀} , {∧} , {∨} , {→}Семантика — это свод правил, наделяющих значением (смыслом) синтаксические конструкции языка.Интерпретации — алгебраические системы, определяющие значения термов и формул.Интерпретации — это математические миры, в которых оценивается выполнимость отношений, представленных логическими формулами.Интерпретация сигнатуры < Const, F unc, P red > — это алгебраическая система I =<DI , Const, F unc, P red >, где— непустое множество, которое называется областью интерпретации , предметной областью , или универсумом ;Const : Const → DI — оценка констант , сопоставляющая каждой константе c элемент(предмет) c из области интерпретации;F unc : F unc(n) → (DIn → DI ) — оценка функциональных символов , сопоставляющая каждомуфункциональномусимволуf (n) местности n всюду определенную n-местную функцию(n)f на области интерпретации;P red : P red(m) → (DIm → {true, f alse}) — оценка предикатных символов, сопоставляющаякаждомупредикатному символу P (m) местности m всюду определенное m-местное отношение(m)Pна области интерпретации.• DI•••Значение терма— рекурсивно (2.25)Отношение выполнимости I |= ϕ(x1 , x2 , .

. . , xn )[d1 , d2 , . . . , dn ]формулы ϕ в интерпретациина наборе d1, d2, . . . , dn определяется рекурсивно (2.27-30)Формула ϕ(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, в которой этаформула выполнима.I2Формула ϕ(x1, . .

. , xn) называется общезначимой (или тождественно истинной ), если этаформула истинна в любой интерпретации.Формула ϕ(x1, . . . , xn) называется противоречивой (или невыполнимой ), если она не является выполнимой.CForm — множество всех замкнутых формул.Модель для множества замкнутых формул Г⊆ CF orm - любая интерпретация I, в которойвыполняются все формулы множества Г.Любая интерпретация является моделью пустого множества Г = ∅Замкнутая формула ϕ является логическим следствием множества замкнутых формулГ (база знаний), если каждая модель для Г является моделью для формулы ϕ, т.е. для любойинтерпретации I |= Г ⇒ I |= ϕ. Обозначается Г |= ϕОбозначение общезначимых формул: |= ϕТеорема о логическом следствии.

Пусть Г= {ψ1 , . . . , ψn } ⊆ CF orm, ϕ ∈ CF orm. ТогдаГ|= ψ ⇔ |= ψ1 ∧ · · · ∧ ψn → ϕ.Существует такая замкнутая формула ϕ, которая истинна в любой интерпретации I с конечной предметной областью DI , но не является общезначимой. ∀x¬R(x, x) ∧ ∀x∀y∀z(R(x, y) ∧R(y, z) → R(x, z)) → ∃x∀y¬R(x, y).Семантическая таблица — это упорядоченная пара множеств формул < Г; ∆ >, Г, ∆ ⊆F orm.

При этом Г — это множество формул, которые мы хотим считать истинными, а ∆ — этомножество формул, которые мы хотим считать ложными.Выполнимая семантическая таблица < Г; ∆ > — такая таблица, что существует такаяинтерпретация I и такой набор значений d1, d2, . . . , dn ∈ DI свободных переменных {x1, x2, . . . , xn}в формулах множеств Г, ∆, для которыхдля любой формулы ϕ, ϕ ∈ ГI 2 ψ(x1 , x2 , . . . , xn )[d1 , d2 , . . .

, dn ] для любой формулы ψ, ψ ∈ ∆• I |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]•.Теорема о табличной проверке общезначимости |= ϕ ⇔невыполнима.Закрытая семантическая таблица <таблица Tϕ=< ∅, {ϕ} >Г, ∆ > — семантическая таблица, у которой Г ∩ ∆ 6=∅Теорема о невыполнимости семантической таблицыца невыполнима.. Закрытая семантическая табли-Атомарная семантическая таблица < Г, ∆ > — семантическая таблица, в которой множества Г и ∆ состоят только из атомарных формул.Теорема о выполнимости семантической таблицы.

Незакрытая атомарная семантическая таблица выполнима.Логический вывод — доказательство общезначимости путем преобразования семантической таблицы Tϕ =< ∅, {ϕ} > к закрытым таблицам.Табличный вывод — такой вывод, в котором участвуют семантические таблицы.3— такой табличный вывод, при котором правила преобразования таблиц (правила табличного вывода) сохраняют выполнимость семантических таблиц.Подстановка — это всякое отображение θ : V ar → T erm, сопоставляющее каждой переменной некоторый терм.Область подстановки Domθ — множество {x : θ(x) 6= x}Конечная подстановка — такая подстановка θ , у которой Domθ — конечное множество.Subst — множество конечных подстановок.Переменная x называется свободной для терма t в формуле ϕ(x), если любое свободноевхождение переменной x в формуле ϕ(x) не лежит в области действия ни одного из квантора,связывающего переменную из множества V art.Подстановка θ = {x1/t1, .

. . , xn/tn} называется правильной для формулы ϕ, если для любойсвязки xi/ti переменная xi свободна для терма ti в формуле ϕ.Правила табличного вывода — 12 правил (4.11-15)Табличный вывод для таблицы T0 — это корневое дерево, вершинами которого служатсемантические таблицы и при этомКорректный табличный вывод1) корнем дерева является таблица T0 ;T— правило табличного вывода.2) из вершины Ti исходят дуги в вершины Tj (Tk ) ⇔ T ,(T)3) листьями дерева могут быть только закрытые и атомарные таблицы.ijkУспешный табличный вывод (табличное опровержение) — табличный вывод, в которомдерево вывода является конечным, а все его листья — закрытые таблицы.Существование успешного вывода означает, что корневая семантическая таблица T0 невыполнима.Лемма о корректности правил вывода.

Каково бы ни было правило табличного выводаL∧, R∧, L∨, R∨, L →, R →, L¬, R¬, L∀, R∀, L∃, R∃ T T,(T ) , таблица T0 выполнима тогда и толькотогда, когда выполнима таблица T1 (или выполнима таблица T2).Теорема корректности табличного вывода. Если для семантической таблицы T0 существует успешный табличный вывод, то таблица T0 невыполнима.Теорема полноты табличного вывода. Если семантическая таблица T0 невыполнима, тодля T0 существует успешный табличный вывод.Теорема Геделя (о полноте).

Если формула ϕ общезначима, то существует успешныйтабличный вывод для таблицы Tϕ =< ∅|ϕ >.Теорема Левенгейма-Сколема. Формула ϕ выполнима ⇔ ϕ имеет модель с конечной илисчетно-бесконечной предметной областью.Теорема компактности Мальцева. Г |= ϕ ⇔ существует такое конечное подмножество00Г , Г ⊆ Г, что Г0 |= ϕЭквиваленция ≡ — выражение ϕ ≡ ψ есть сокращенная запись (ϕ → ψ) ∧ (ψ → ϕ)Формулы ϕ и ψ называются равносильными, если формула ϕ ≡ ψ общезначима, то есть|= ϕ ≡ ψ .0142Отношение равносильности — это отношение эквивалентности.Если ϕ общезначима(выполнима) и ϕ ≡ ψ, то и ψ общезначима (выполнима).Запись ϕ[ψ] означает, что формула ϕ содержит подформулу ψ.Запись ϕ[ψ/χ] обозначает формулу, которая образуется из формулы ϕ заменой некоторых(не обязательно всех) вхождений подформулы ψ на формулу χ.Теорема о равносильной замене.