Теормин 2014 (микро) (Мадорский)

¬, ∀, ∃&∨→Тройка <Const , Pred , Func> называется сигнатурой алфавита. ϕ(x1, x2, . . . , xn) — запись, обозначающая формулу ϕ, укоторой Var ϕ⊆ {x1, x2, . . . , xn}. Если Varϕ = ∅, то формула ϕ называется замкнутой формулой, или предложением.CForm — множество всех замкнутых формул.Формула ϕ(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ϕ = <∅; {ϕ}> к закрытой называются логическим выводом. Если ввыводе участвуют семантические таблицы, то логический вывод называется табличным семантическим выводом.Табличный вывод – это корневое дерево, в котором корнем является сама таблица, дуги выходят в соответствии справилами табличного вывода, а листьями служат либо закрытые таблицы, либо атомарные таблицыУспешный табличный вывод – если дерево вывода – конечно и все его листья – закрытые таблицыТеорема корректности табличного вывода: Если для таблицы существует успешный табличный вывод, то онаневыполнима (следует из определения, леммы о корректности правил [Каково бы ни было правило табличноговывода, исходная таблица выполнима <=> выполнима таблица, порождённая правилом (одна или обе, если их 2)] иутверждения о невыполнимости закрытых таблиц).Следствие: Если для таблицы T=<∅|ϕ> можно построить успешный табличный вывод, то |= ϕТеорема полноты табличного вывода: Если семантическая таблица T0 невыполнима, то для T0 существует успешныйтабличный вывод.Теорема Геделя (о полноте): Если формула ϕ общезначима, то существует успешный табличный вывод для таблицы Tϕ= <∅|ϕ>.

(следует из теоремы полноты табличного вывода)Теорема Левенгейма-Сколема: Формула ϕ выполнима ⇐⇒ ϕ имеет модель с конечной или счетно-бесконечнойпредметной областью. (Если ϕ выполнима, то тогда бы нашлась в соответствии с теоремой о полноте табличноговывода либо атомарная незакрытая таблица, либо счётная ветвь в табличном выводе)Теорема Компактности Мальцева: Γ |= ϕ ⇐⇒ существует такое конечное подмножество Γ’, Γ’⊆ Γ, что Γ’|= ϕ.(следствие означает соответствующую невыполнимость таблицы, т.е. наличие успешного табличного вывода, т.е. егоконечность, т.е. количество формул к которым был применён табличный вывод – конечно, а значит остальное можнообрезать и для нового конечного набора формул – этот табличный вывод останется верным)Теорема о равносильной замене: |= ψ≡χ => |= ϕ[ψ] ≡ ϕ[ψ/χ] (Доказывается индукцией по числу связок икванторов в формуле ϕ)Предварительная нормальная форма (ПНФ) – ϕ= Q1x1Q2x2…Qnxn M(x1, x2, …, xn)Теорема о ПНФ: Для любой замкнутой формулы существует предварительная нормальная формула(Переименование переменных, потом удаление импликации, потом продвижение отрицания вглубь, вынесениекванторов наружу, приведение к КНФ)Сколемовская стандартная форма (ССФ) – ∀1x1∀2x2…∀nxn M(x1, x2, …, xn) (без ∃)Теорема о ССФ: Для любой замкнутой формулы существует такая сколемовская стандартная формула, что оноодна выполнима тогда и только тогда, когда выполнима другая (через лемму об удалении кванторовсуществования)Теорема: Сколемовская стандартная форма невыполнима тогда и только тогда, когда множество формул (всеотдельные конъюнкции с кванторами ∀) не имеет моделиНевыполнимая, противоречивая система дизъюнктов – система не имеющая ни одной модели, в которой бывыполнялись все дизъюнктыМетод резолюций:Проверка общезначимости формулы ϕ сводится к проверке противоречивости системы дизъюнктов Sϕ.Этап 1.

Сведение проблемы общезначимости к проблеме противоречивости: ϕ -> ϕ0 = ¬ϕЭтап 2. Построение предваренной нормальной формы (ПНФ). ϕ0 -> ϕ1 = Q1x1Q2x2. . . Qnxn(D1&D2& . . . &DN)Этап 3. Построение сколемовской стандартной формы (ССФ). ϕ1 -> ϕ2 = ∀xi1∀xi2.

. . ∀xik(D1&D2& . . . &DN)Этап 4. Построение системы дизъюнктов. ϕ2 -> Sϕ = {D1, D2, . . . , DN},ϕ общезначимая ⇐⇒ система дизъюнктов Sϕ противоречива.Эрбрановские интерпретации — это специальная разновидность интерпретаций, в основе которых лежат свободныеалгебры.Пусть задана некоторая сигнатура σ = <Const, Func, Pred>. Тогда эрбрановским универсумом σ называется множествотермов Hσ= ⋃∞=0 , где i = 0 H0 ={Const , если Const ≠ ∅; {c}, если Const = ∅ (эрбрановская константа)}, i → i + 1 Hi +1 =(k)Hi∪ {f (t1, . .

. , tk): f(k)∈ Func, t1, . . . , tk ∈ Hi}Эрбрановский универсум — это множество всех термов, которые можно построить из констант и функциональныхсимволов заданной сигнатуры (т.е. это предметная область эрбрановских интерпретаций). Термы эрбрановскогоуниверсума не содержат переменных и называются основными термами.Эрбрановская H-интерпретация IH = <Hσ, ConstH(с верхн. подчёрк), FuncH(с верхн. подчёрк), Pred(с верхн. подчёрк)>сигнатуры σ = <Const , Func , Pred> состоит из• стандартной предметной области — эрбрановского универсума Hσ• стандартной оценки констант: ConstH(c) = c, т. е.

значением каждого константного символа c является егособственное изображение• стандартной оценки функциональных символов: FuncH(f(n)) = f : f (t1, t2, . . . , tn) = f(n)(t1, t2, . . . , tn),т. е. каждыйфункциональный символ f играет рольконструктора термов эрбрановского универсума• произвольной оценки предикатных символов.Теорема о H –интерпретациях: Система дизъюнктов S выполнима тогда и только тогда, когда S имеет эрбрановскуюмодель, т.е. выполнима хотя бы в одной H -интерпретации. (В одну сторону очевидно, а в другую – построимгомоморфное отображение) Следствие: Система дизъюнктов S противоречива тогда и только тогда, когда Sневыполнима ни в одной эрбрановской интерпретации.Пусть P(m) ∈ Pred, и t1, .

. . ,tm ∈ Hσ — набор основных термов. Тогда формула P(m)(t1, . . . , tm) называется основныматомом. Множество всех основных атомов называется эрбрановским базисом и обозначается BH. Всякая Hинтерпретация I задается подмнож. BI истинных осн. атомов: BI= {P(m)(t1, . . . ,tm) : I |= P(m)(t1, . . . ,tm), {t1, . . . , tm} ⊆ H}.Пусть имеется дизъюнкт D = ∀x1…∀xm (L1 ∨…∨ Lk) и набор основных термов t1, .