Теормин 2014 (микро) (Мадорский) (1158135)
Текст из файла
¬, ∀, ∃&∨→Тройка <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, .
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
