Вопрос 3. Логика 1-го порядка. Выполнимость и общезначимость. Общая схема метода резолюций. (1161605)
Текст из файла
Основыматематическойлогики и логическогопрограммированияВладимир Анатольевич Захаровzakh@cs.msu.suhttp://mathcyb.cs.msu.su/courses/logprog.htmlБилет 1.Классическая логика предикатовпервого порядка.Выполнимые и общезначимыеформулы.Метод резолюции проверкиобщезначимости формул.АЛФАВИТБазовые символы.Предметные переменныеVar = {x1 , x2 , . . . , xk , . . . };Предметные константыConst = {c1 , c2 , . . . , cl , .
. . };Функциональные символыFunc = {f1Предикатные символыPred = {P1(n1 )(n2 ), f2(m1 )(m2 ), P2(nr ), . . . , fr, . . . };(ms ), . . . , PsТройка hConst, Pred, Funci называется сигнатурой алфавита., . . . }.АЛФАВИТЛогические связки и кванторы.КонъюнкцияДизъюнкцияОтрицаниеИмпликация(логическое(логическое(логическое(логическоеКвантор всеобщностиКвантор существованияЗнаки препинания.РазделительСкобки,()И)ИЛИ)НЕ)ЕСЛИ-ТО)&∨¬→.(«для каждого»)(«хотя бы один»)∀∃СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫОпределение терма.Терм — этоxcf (n) (t1 , t2 , .
. . , tn ), если x ∈ Var, если c ∈ Const, если f (n) ∈ Funct1 , t2 , . . . , tn — термыx — переменная;c — константа;составной терм.Term — множество термов заданного алфавита.Vart — множество переменных, входящих в состав терма t.t(x1 , x2 , . . . , xn ) — запись обозначающая терм t, у которогоVart ⊆ {x1 , x2 , . .
. , xn }.СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫОпределение формулы.Формула — этоатомарная формулаP (m) (t1 , t2 , . . . , tm )составная формула(ϕ&ψ)(ϕ ∨ ψ)(ϕ → ψ)(¬ϕ)(∀xϕ)(∃xϕ), если P (m) ∈ Pred, {t1 , t2 , . . . , tm } ⊆ Term;, если ϕ, ψ — формулы;, если x ∈ Var , ϕ — формула.Form — множество всех формул заданного алфавита.СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫСвободные и связанные переменные.Квантор связывает ту переменную, которая следует за ним.Вхождение переменной в области действия квантора,связывающего эту переменную, называется связанным .Вхождение переменной в формулу, не являющееся связанным,называется свободным .Переменная называется свободной , если она имеет свободноевхождение в формулу.СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫСвободные и связанные переменные.Varϕ — множество свободных переменных формулы ϕ.mSVarti ;ϕ = P (m) (t1 , t2 , .
. . , tm ) Varϕ =i=1ϕ = (ψ1 &ψ2 )ϕ = (ψ1 ∨ ψ2 )ϕ = (ψ1 → ψ2 )Varϕ = Varψ1 ∪ Varψ2 ;ϕ = (¬ψ)Varϕ = Varψ ;ϕ = (∀xψ)ϕ = (∃xψ)Varϕ = Varψ \ {x}.СИНТАКСИС: ТЕРМЫ И ФОРМУЛЫϕ(x1 , x2 , . . . , xn ) — запись, обозначающая формулу ϕ, у которойVarϕ ⊆ {x1 , x2 , . . . , xn }.Если Varϕ = ∅, то формула ϕ называетсязамкнутой формулой , или предложением .CForm — множество всех замкнутых формул.Соглашение о приоритете логических операцийВ порядке убывания приоритета связки и кванторырасполагаются так:¬, ∀, ∃&∨→СЕМАНТИКА: ИНТЕРПРЕТАЦИИИнтерпретация сигнатуры hConst, Func, Predi — этоалгебраическая система I = hDI , Const, Func, Predi, гдеIIIIDI — непустое множество, которое называется областьюинтерпретации , предметной областью , или универсумом ;Const : Const → DI — оценка констант ,сопоставляющая каждой константе c элемент (предмет) c̄из области интерпретации;Func : Func (n) → (DIn → DI ) — оценкафункциональных символов , сопоставляющая каждомуфункциональному символу f (n) местности n всюдуопределенную n-местную функцию f̄ (n) на областиинтерпретации;Pred : Pred (m) → (DIm → {true, false}) — оценкапредикатных символов , сопоставляющая каждомупредикатному символу P (m) местности m всюдуопределенное m-местное отношение P̄(m) на областиинтерпретации.СЕМАНТИКА: ИНТЕРПРЕТАЦИИЗначение термаПусть заданы интерпретация I = hDI , Const, Func, Predi, термt(x1 , x2 , .
. . , xn ) и набор d1 , d2 , . . . , dn элементов (предметов) изобласти интерпретации DI .Значение t(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] терма t(x1 , x2 , . . . , xn )на наборе d1 , d2 , . . . , dn определяется рекурсивно.IЕсли t(x1 , x2 , . . .
, xn ) = xi , тоt(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] = di ;IЕсли t(x1 , x2 , . . . , xn ) = c, тоt(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] = c̄;IЕсли t(x1 , x2 , . . . , xn ) = f (t1 , . . . , tk ), тоt(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ] =f̄(t1 [d1 , d2 , . . . , dn ], . . . , tk [d1 , d2 , . . . , dn ]).СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛОтношение выполнимости формулЗначение формул в интерпретации определяется при помощиотношения выполнимости |=.Пусть заданы интерпретация I = hDI , Const, Func, Predi,формула ϕ(x1 , x2 , . .
. , xn ) и набор d1 , d2 , . . . , dn элементов(предметов) из области интерпретации DI .Отношение выполнимости I |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]формулы ϕ в интерпретации I на наборе d1 , d2 , . . . , dnопределяется рекурсивно.IЕсли ϕ(x1 , x2 , . . . , xn ) = P(t1 , . . . , tm ), тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . .
, dn ]⇐⇒P̄(t1 [d1 , d2 , . . . , dn ], . . . , tm [d1 , d2 , . . . , dn ]) = true;СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛОтношение выполнимости формулIЕсли ϕ(x1 , x2 , . . . , xn ) = ψ1 &ψ2 , тоII |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]⇐⇒I |= ψ1 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]I |= ψ2 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]Если ϕ(x1 , x2 , . . . , xn ) = ψ1 ∨ ψ2 , тоI |= ϕ(x1 , x2 , .
. . , xn )[d1 , d2 , . . . , dn ]⇐⇒I |= ψ1 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]илиI |= ψ2 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛОтношение выполнимости формулIЕсли ϕ(x1 , x2 , . . . , xn ) = ψ1 → ψ2 , тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , .
. . , dn ]⇐⇒I 6|= ψ1 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]илиI |= ψ2 (x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]IЕсли ϕ(x1 , x2 , . . . , xn ) = ¬ψ, тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]⇐⇒I 6|= ψ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]СЕМАНТИКА: ВЫПОЛНИМОСТЬ ФОРМУЛОтношение выполнимости формулIЕсли ϕ(x1 , x2 , . .
. , xn ) = ∀x0 ψ(x0 , x1 , x2 , . . . , xn ), тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]⇐⇒для любого элемента d0 , d0 ∈ DI , имеет местоI |= ψ(x0 , x1 , x2 , . . . , xn )[d0 , d1 , d2 , . . . , dn ]IЕсли ϕ(x1 , x2 , . . . , xn ) = ∃x0 ψ(x0 , x1 , x2 , . . . , xn ), тоI |= ϕ(x1 , x2 , . . . , xn )[d1 , d2 , . . . , dn ]⇐⇒для некоторого элемента d0 , d0 ∈ DI , имеет местоI |= ψ(x0 , x1 , x2 , . .
. , xn )[d0 , d1 , d2 , . . . , dn ]ВЫПОЛНИМЫЕ И ОБЩЕЗНАЧИМЫЕФОРМУЛЫФормула ϕ(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 → ϕ.Доказательство. ⇒ Пусть I — произвольная интерпретация.Если I 6|= ψ1 & . . . &ψn , то I |= ψ1 & . . . &ψn → ϕ.Если I |= ψ1 & . . . &ψn , то I |= ψi , 1 ≤ i ≤ n, т. е. I — модельдля Γ. Поскольку Γ |= ϕ, получаем I |= ϕ.Значит, I |= ψ1 & . . . &ψn → ϕ.Таким образом, для любой интерпретации I имеет местоI |= ψ1 & . . . &ψn → ϕ.Значит, ψ1 & . . .
&ψn → ϕ — общезначимая формула.МОДЕЛИ. ЛОГИЧЕСКОЕ СЛЕДСТВИЕТеорема о логическом следствииПусть Γ = {ψ1 , . . . , ψn } ⊆ CForm, ϕ ∈ CForm. ТогдаΓ |= ϕ ⇐⇒ |= ψ1 & . . . &ψn → ϕ.Доказательство. ⇐ Пусть I — модель для множествапредложений Γ, т. е. I |= ψi , 1 ≤ i ≤ n.Тогда I |= ψ1 & . . . &ψn .Так как ψ1 & . . . &ψn → ϕ — общезначимая формула, имеетместо I |= ψ1 & .
. . &ψn → ϕ.Значит, I |= ϕ.Так как I — произвольная модель для Γ, приходим кзаключению Γ |= ϕ.ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛОбщезначимые формулы — это каналы причинно-следственнойсвязи, по которым передаются знания, представленные в виделогических формул, преобразуясь при этом из одной формы вдругую.Практически важно уметь определять эти каналы инастраивать их на извлечение нужных знаний.IБаза знаний — множество предложений Γ;IЗапрос к базе знаний — предложение ϕ;IПолучение ответа на запрос — проверка логическогоследствия Γ |= ϕ.Если Γ — конечное множество, то проверка логическогоследствия сводится к проверке общезначимости формулыψ1 & . . . &ψn → ϕ .ПРОБЛЕМА ОБЩЕЗНАЧИМОСТИ ФОРМУЛТаким образом, возникает проблемаобщезначимости формул:Для заданной формулы ϕпроверить ее общезначимость:|= ϕ?ОБЩАЯ СХЕМА МЕТОДА РЕЗОЛЮЦИЙЗадача проверки общезначимости формул логики предикатов.|= ϕ ?Этап 1.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
