Подготовка к экзамену

Задача 5.

Какая формула ϕ называется логическим следствием множества предложений Γ? Существует ли хотя бы одна такая формула, которая является логическим следствием любого множества предложений Γ? Приведите пример замкнутой формулы ϕ, которая не является логическим следствием множества

замкнутых формул Γ = {∃xP(x), ∀x¬P(x)}?

Ответ: логическое следствие <=> каждая модель Г является моделью для phi (в определении сказано, что речь идёт о замкнутых формулах), очевидно что общезначимая формула будет лог. следствием любого Г.

Пример замкнутой формулы ф: множество противоречиво => любая замкнутая формула является логическим следствием => нельзя привести примера

______________________________________________________________________________

Задача 6.

Какова формулировка теоремы об эрбрановских интерпретациях? Верно ли, что каждая непротиворечивая система дизъюнктов имеет хотя бы одну эрбрановскую модель?

Теорема: Система дизъюнктов S выполнима тогда и только тогда, когда S имеет эрбрановскую модель, т.е. выполнима хотя бы в одной H-интерпретации.

“И, как будет показано, для проверки противоречивости систем дизъюнктов достаточно ограничиться рассмотрением H-интерпретаций” - соответственно, да

______________________________________________________________________________

Задача 7.

Какова формулировка теоремы корректности операционной семантики относительно декларативной семантики? Верно ли, что из этой теоремы следует, что для любого атома из наименьшей эрбрановской модели MP программы P запрос? A, обращенный к программе P имеет успешное вычисление?

Любой вычисленный ответ является правильным. (2го вопроса не будет, т.к. он сказал что выкинул модели программ из курса)

______________________________________________________________________________

Задача 8.

Какова формулировка теоремы Черча о проблеме общезначимости в классической логике предикатов? Следует ли из этой теоремы, что не существует алгоритма, проверяющего выполнимость формул логики предикатов?

Теорема: Следствие 2 (Теорема Черча).

Не существует алгоритма, способного определить по заданной замкнутой формуле логики предикатов ϕ, является ли эта формула общезначимой, т. е. проблема

общезначимости "|= ϕ ?" алгоритмически неразрешима.

Да, следует,т.к. проблема выполнимости phi <=> проблема общезначимости !phi.

______________________________________________________________________________

Задача 9. Как формулируется задача верификации моделей программ (model checking)? К каким задачам теории графов сводится задача model-checking для темпоральной логики PLTL?

Для любой PLTL fi и CLS M проверить M |= fi (для любой трассы tr,tr принадлежит Tr0(M),имеет место I(tr),0 |= fi).

Поиск компонент связанности.

______________________________________________________________________________

Задача 5.

Какая семантическая таблица 〈Γ, ∆〉 называется выполнимой ? Является ли выполнимой семантическая таблица 〈{P (x)}, {P (y)}〉?

Семантическая таблица 〈Γ, ∆〉 называется выполнимой, если существует такая I и d₁...d_n принадлежащие D_I ,что для любой фи из Г выполняется, что I |= фи(x1,...,xn)[d1...dn] и для любой пси из ∆ выполняется что I |=/=пси(x1,..,xn)[d1..dn].

Таблица 〈{P (x)}, {P (y)}〉 выполнима т.к. она атомарна и не закрыта.

для тех, кто не верит:

пример: d1, d2, P(d1)=true, P(d2) = false, x=d1, y=d2... вот интерпретация и набор значений свободных переменных, для которых все формулы из Г истинны, а из Д - ложны, значит выполнима.

______________________________________________________________________________

Задача 6.

Что такое эрбрановский универсум? Каким условиям должна удовлетворять сигнатура σ для того, чтобы эрбрановский универсум сигнатуры σ был конечным множеством?

H - эрбраноj,вский универсум сигнатуры <Const,Func,Pred> - это множество H=U^oo₀ Hi,где

H0=либо Const, если Const непустое, либо {c} (эрбрановская константа), если Const-пустое; Hi=Hi-1 U {f⁽ⁿ⁾(t1...tn), где f принадлежит Func, t1...tn - принадлежат Hi-1}.

Чтоб универсум был конечен Func должно быть пустым, и Const - конечным.

______________________________________________________________________________

Задача 7.

Какая интерпретация называется эрбрановской моделью для хорновской логической программы P? Верно ли то, что всякая хорновская логическая программа имеет непустую эрбрановскую модель?

Эрбрановская интерпретация I для логической программы P называется её моделью, если она является моделью для любого хорновского дизъюнкта, входящего в неё.

Да, верно. (Этого не будет на экзамене)

______________________________________________________________________________

Задача 8.

Сформулируйте правило SLDNF-резолюции. Какой ответ будет получен на запрос ?not(P (x)) к программе P = {P (c) ← R(c)}?

Пусть имеется G:?not(C1),C2...Cn к программе P.

Для вычисления SLDNF-резольвенты G1:

1. формируется запрос G`:?C1 к программе P

2. проводится построение дерева вычислений T для запроса G`

3. возможен 1 из 3х исходов:

-Успех, если все ветви дерева завершились failure

-Failure, если хотя бы одна ветвь дерева завершилась Успехом

-Бесконечность, если дерево бесконечно и не было обнаружено успешных вычислений.

В реальности, это не совсем так, результат зависит от порядка выбора программных правил.

Построится дерево для запроса ?P(X), которое завершится failure. Тогда для исходного запроса будет вычислен ответ, являющийся пустой подстановкой.

Никакого, т.к. программа зациклица (неверно, ответа не будет т.к. нет правила для R(c)).

______________________________________________________________________________

Задача 9.

Как определяется интерпретация темпоральной логики линейного времени PLTL ? Являются ли равносильными PLTL формулы Fp и (p ∨ ¬p)Up?

I=<N,<=,кси>

N - {0,1,2...}-моменты времени

<= - отношение нестрогого линейного порядка на N

кси : N x AP -> {true,false} - оценка атомарных высказываний на времени

Да, являются равносильными, обе утверждают “В какой-то момент времени в будущем будет верно p”

______________________________________________________________________________

Задача 5 (2 балла).

Теорема корректности: если семантическая таблица имеет успешный табличный вывод, то она невыполнима.

Корректно.d

∀x φ (x) ≡ ~(∃x ~φ(x)) => можно перекинуть.

Задача 6 (2 балла).

Т. Мальцева. Произвольное множество формул обладает моделью тогда и только тогда, когда каждое конечное подмножество обладает моделью.

Или

Если Г|=φ, то существует конечное подмножество Г, называемое Г’, такое что Г’|=φ.

Теорема Эрбрана. Система дизъюнктов S = {D₁;...;D_т} противоречива тогда и только тогда, когда существует конечное противоречивое множество G0 основных примеров дизъюнктов S.

Да, следует.

Задача 7 (2 балла).

Если P - программа, а G - запрос, и Theta (некая подстановка) - ответ, то Theta - правильный ответ, если

P |= \/Z1 … \/Zn GTheta, где Z1,...Zn - переменные Theta

правильный ответ = ответ, логически следующий из программы

основной атом - не содержит переменных => запрос не содержит целевых переменных =>

1. либо единственный ответ на него есть пустая подстановка (если атом является логическим следствием программы)

2. либо нет правильных ответов (в противном случае)

=> правильных ответов может быть 0 либо 1.

Задача 8 (2 балла).

Значит, что класс функций, вычислимых с помощью программ ХЛП, в точности совпадает с классом функций, вычислимых на машине тьюринга.

Очевидный ответ - нет, то что выдает программа с отсечениями - подмножество программы без отсечений. Тут не очевидно, ведь спрашивается не про ту же самую программу, но с убранными отсечениями, а про некую другую программу. Но мне кажется, что всё-таки ответ “нет”, ибо иначе не пришлось бы выдумывать операторы отсечения и not.

Задача 9 (2 балла).

I,w |= ⇫фи <=> для любого w’ : если (w,w’) принадлежит R , то I,w’ |= фи

Верно потому что:

I,w |=/=⇫ -p <=> I,w |= -⇫-p <=> I,w |= ромбик p

______________________________________________________________________________

Ответ 5:

Для любой невыполнимой семантической таблицы существует успешный табличный вывод.

Она не общезначима и ее отрицание так же не общезначимо (<fi,> == <,~fi>) => она выполнима.

Ответ 6:

Для сигнатуры c=<Const,Func,Pred> эрбановской интерпретацией называется I=(Hi,Const, Func, Pred)

где Hi - эрбрановский универсум

Const (c) = c

Func (f⁽ⁿ⁾)=f: f(t1,...tn) = f⁽ⁿ⁾(t1..tn)

Pred - задаются произвольно

Ответ в 6й - 16 (2^4) потому что двухместный предикат P можно записать как P(c1,c1)P(c2,c2)P(c2,c1),P(c1,c2) и перебрать все возможные значения: каждый вариант может быть 0 и 1 - соотв 16 наборов из 0и1 длины 4. Надеюсь так всем понятно??)))

Ответ 7:

SLD-резолютивным вычислением называется последовательность троек

<Dj1,Theta1,G1>...<Djn,Thetan,Gn>...

где

1. Theta i принадлежит Subst, Dji принадлежит P, Gi - целевое утверждение

2. Gi - SLD резольвента утв Dji и Gi-1 c унификатором Theta i

Ответ 8:

Для любой функции выбора подцели вычислимый ответ совпадает с правильным с точностью до подстановки. Любой правильный ответ является частным случаем какого-то из вычисленных.

R(X)<-R(X) - бесконечная

Ответ 9:

I,w |= fi -> psi <=> для любого w`, если (w,w`) принадлежит R и I,w’ |=/=fi, то I,w’ |= psi

p-> p - общезначимая

________________________________________________________

Задача 5 (2 балла).

Сформулируйте теорему компактности Мальцева. Следует ли из этой теоремы утверждение: Если бесконечное множество предложений Γ не имеет модели, то хотя бы одно предложение множества Γ является противоречивым ?

Два варианта (хз, эквивалентны они, или это две разные теоремы):

• Г |= fi <=> exsist конечное подмножество Г’ in Г: Г’ |= fi.

• Если Г - противоречиво, то существует конечное под-во которое противоречиво.

Да нифига... Не следует. То что существует конечная система, не значит что эта система размерности 1.

___________________________________________________________

Задача 5 (2 балла).

Какая семантическая таблица T = 〈Γ, ∆〉 называется выполнимой? Может ли выполнимая таблица содержать только невыполнимые формулы?

Ответ: семантическая таблица T = 〈Γ, ∆〉 называется выполнимой, если существует такая интерпретация I и такой набор значений

Если Γ=ϕ => то может.

Может ли выполнимая таблица содержать только невыполнимые формулы? <<<=

Пример : <0|false>