Задачи (Старые варианты экзамена), страница 4

Как определяется частичная корректность программы π относительнопредусловия ϕ и постусловия ψ в интерпретации I?Является ли программа while X > 0 do X + + od частично корректной относительно предусловияϕ = (X > 0) и постусловия ψ = (X < 0) в стандартной интерпретации арифметики целых чисел?Задача 9 (2 балла).

Как определяется отношение выполнимости I, s0 |= ϕUψ в темпоральнойлогике PLTL? Являются ли формулы ϕU(ψ1 &ψ2 ) и ϕUψ1 & ϕUψ2 равносильными?Задача 9. Как формулируется задача верификации моделей программ (model checking)? К какимзадачам теории графов сводится задача model-checking для темпоральной логики PLTL?Êàê â èíòóèöèîíèñòñêîé ëîãèêå îïðåäåëÿåòñÿ îòíîøåíèå âûïîëíèìîñòè I, w |=ϕ → ψ äëÿ èìïëèêàòèâíîé ôîðìóëû? Óêàæèòå, êàêèå èç ôîðìóë p ∨ ¬p è p → p ÿâëÿþòñÿ îáùåçíà÷èìûìè ôîðìóëàìè èíòóèöèîíèñòñêîé ëîãèêè?Çàäà÷à 9 (2 áàëëà).

Êàê îïðåäåëÿåòñÿ îòíîøåíèå âûïîëíèìîñòè I, t |= ϕUψ â òåìïîðàëüíîé ëîãèêåPLTL? Âåðíî ëè, ÷òî ôîðìóëû ϕU(ψ1 ∨ ψ2) è (ϕUψ1) ∨ (ϕUψ2) ÿâëÿþòñÿ ðàâíîñèëüíûìè ôîðìóëàìèëîãèêè PLTL?Çàäà÷à 9 (2 áàëëà).Задача 9 (2 балла). Как определяется интерпретация интуиционистской логики высказываний?Является ли формула p → ¬¬p общезначимой в интуиционистской логике высказываний?Задача 9. Как определяется интерпретация темпоральной логики линейного времени PLTL ? Являютсяли равносильными PLTL формулы Fp и (p ∨ ¬p)Up?Задача 9 (2 балла). Как определяется частичная корректность программы π относительно предусловия ϕ и постусловия ψ в интерпретации I?Является ли программа while X > 0 do X + + od частично корректной относительно предусловияϕ = (X > 0) и постусловия ψ = (X < 0) в стандартной интерпретации арифметики целых чисел?Задача 9 (2 балла).

Как определяется отношение выполнимости I, s0 |= ϕUψ в темпоральнойлогике PLTL? Являются ли формулы ϕU(ψ1 &ψ2 ) и ϕUψ1 & ϕUψ2 равносильными?Задача 9 (2 балла). Как определяется отношение выполнимости I, w |= ϕ в модальной логике?Верно ли, что для любой модели Крипке I и для любого состояния w если I, w 6|= ¬p, то I, w |= ♦p ?Задача 9 (2 балла). Как определяется отношение выполнимости I, s0 |= Fψ в темпоральной логикеPLTL? Являются ли формулы F(ψ1 &ψ2 ) и Fψ1 & Fψ2 равносильными?Задача 10 (3 балла). Известно, что некоторая модель для формулы ϕ не является моделью дляформулы ψ. Какие из приведенных ниже утверждений всегда верны для любых замкнутых формул ϕиψ?1.

Формула ϕ является логическим следствием формулы ψ, потому что...2. Формула ψ является логическим следствием формулы ϕ, потому что...3. Не существует успешного табличного вывода из таблицы T 0 = h{ψ}, {ϕ}i, потому что...4. Не существует успешного табличного вывода из таблицы T = h{ϕ}, {ψ}i, потому что...5. Все приведенные выше утверждения в общем случае неверны, потому что...Задача 10 (3 балла). Известно, что для семантической таблицы T = h{ϕ}, {ψ}i нельзя построитьни одного успешного табличного вывода. Какие из приведенных ниже утверждений всегда верны длялюбых замкнутых формул ϕ и ψ ?1. Таблица T = h{ϕ}, {ψ}i не является выполнимой, потому что...2.

Для таблицы T 0 = h{ψ}, {ϕ}i также не существует ни одного успешного табличного вывода,потому что...3. Формула ϕ не является логическим следствием формулы ψ, потому что...4. Формула ψ не является логическим следствием формулы ϕ, потому что...5. Все приведенные выше утверждения в общем случае неверны, потому что...Задача 10. Известно, что выполнимые замкнутые формулы ϕ и ψ не имеют ни одной общей модели.Какие из приведенных ниже утверждений всегда верны и почему?1.

Существует формула χ, логическим следствием которой являются обе формулы ϕ и ψ, потомучто ...2. Существует формула χ, которая является логическим следствием обеих формул ϕ и ψ, потомучто ...3. Не существует ни одного успешного табличного вывода из семантической таблицы h{ϕ}, {ψ}i,потому что ...4. Все приведенные выше утверждения верны.Ïðåäïîëîæèì, ÷òî äàíû äâà òàêèå ìíîæåñòâà çàìêíóòûõ ôîðìóë Γ1 è Γ2,äëÿ êîòîðûõ íå ñóùåñòâóåò íè îäíîãî ïðåäëîæåíèÿ ϕ, óäîâëåòâîðÿþùåãî îäíîâðåìåííî ñîîòíîøåíèÿìΓ1 |= ϕ è Γ2 |= ϕ. Âûáåðèòå òå óòâåðæäåíèÿ, êîòîðûå â ýòîì ñëó÷àå âñåãäà ñïðàâåäëèâû è îáîñíóéòåñäåëàííûé âûáîð.1.

Γ1 ∩ Γ2 = ∅, ïîòîìó ÷òî ...2. Γ1 = ∅ èëè Γ2 = ∅, ïîòîìó ÷òî ...3. Îáà ìíîæåñòâà Γ1 è Γ2 íåïðîòèâîðå÷èâû, ïîòîìó ÷òî ...4. Òàêîé ïàðû ìíîæåñòâ Γ1 è Γ2, óäîâëåòâîðÿþùåé ïðåäïîëîæåíèþ, íå ñóùåñòâóåò, ïîòîìó ÷òî ...5. Íè îäíî èç ïðèâåäåííûõ âûøå óòâåðæäåíèé â îáùåì ñëó÷àå íå âåðíî, ïîòîìó ÷òî...Çàäà÷à 10 (3 áàëëà).Ïðåäïîëîæèì, ÷òî áåñêîíå÷íîå ìíîæåñòâî çàìêíóòûõ ôîðìóë Γ îáëàäàåò òåìñâîéñòâîì, ÷òî äëÿ ëþáîé ôîðìóëû ϕ, ϕ ∈ Γ, ñåìàíòè÷åñêàÿ òàáëèöà hΓ \ {ϕ}, {ϕ}i íå èìååò íè îäíîãîóñïåøíîãî òàáëè÷íîãî âûâîäà. Êàêèå èç ïðèâåäåííûõ íèæå óòâåðæäåíèé âñåãäà âåðíû äëÿ óêàçàííîãîìíîæåñòâà Γ ?1.

Íå ñóùåñòâóåò óñïåøíîãî òàáëè÷íîãî âûâîäà èç òàáëèöû hΓ, ∅i, ïîòîìó ÷òî...2.  ìíîæåñòâå Γ íåò îáùåçíà÷èìûõ ôîðìóë, ïîòîìó ÷òî...3. Ìíîæåñòâî ôîðìóëà Γ íå èìååò ìîäåëè, ïîòîìó ÷òî...4. Òàêîãî ìíîæåñòâà ôîðìóë Γ, óäîâëåòâîðÿþùåãî óêàçàííûì óñëîâèÿì, íå ñóùåñòâóåò, ïîòîìó÷òî...5.

Âñå ïðèâåäåííûå âûøå óòâåðæäåíèÿ â îáùåì ñëó÷àå íåâåðíû.Çàäà÷à 10 (3 áàëëà).Задача 10 (3 балла). Известно, что некоторая модель для формулы ϕ не является моделью дляформулы ψ. Какие из приведенных ниже утверждений всегда верны для любых замкнутых формул ϕиψ?1. Формула ϕ является логическим следствием формулы ψ, потому что...2. Формула ψ является логическим следствием формулы ϕ, потому что...3. Не существует успешного табличного вывода из таблицы T 0 = h{ψ}, {ϕ}i, потому что...4.

Не существует успешного табличного вывода из таблицы T = h{ϕ}, {ψ}i, потому что...5. Все приведенные выше утверждения в общем случае неверны, потому что...Задача 10. Пусть известно, что семантическая таблица hΓ, ∅i для классической логики предикатов имееттабличный вывод, одна из ветвей которого заканчивается такой семантической таблицей hΓ0 , ∆0 i, что Γ0 ∩∆0 =∅ и при этом ни одно правило табличного вывода не применимо к таблице hΓ0 , ∆0 i. Какие из приведенныхниже утверждений наверняка справедливы и почему?1. Множество формул Γ не имеет модели, потому что...2. Множество формул Γ имеет модель с бесконечной предметной областью, потому что...3.

Во множестве формул Γ обязательно есть хотя бы одна общезначимая формула, потому что...4. Во множестве формул Γ обязательно есть хотя бы одна противоречивая формула, потому что...5. Ни одно из приведенных выше утверждений не верно, потому что...Задача 10 (3 балла). Известно, что некоторая модель для формулы ϕ не является моделью дляформулы ψ.

Какие из приведенных ниже утверждений всегда верны для любых замкнутых формул ϕиψ?1. Формула ϕ является логическим следствием формулы ψ, потому что...2. Формула ψ является логическим следствием формулы ϕ, потому что...3. Не существует успешного табличного вывода из таблицы T 0 = h{ψ}, {ϕ}i, потому что...4. Не существует успешного табличного вывода из таблицы T = h{ϕ}, {ψ}i, потому что...5.

Все приведенные выше утверждения в общем случае неверны, потому что...Задача 10 (3 балла). Известно, что для семантической таблицы T = h{ϕ}, {ψ}i нельзя построитьни одного успешного табличного вывода. Какие из приведенных ниже утверждений всегда верны длялюбых замкнутых формул ϕ и ψ ?1. Таблица T = h{ϕ}, {ψ}i не является выполнимой, потому что...2. Для таблицы T 0 = h{ψ}, {ϕ}i также не существует ни одного успешного табличного вывода,потому что...3. Формула ϕ не является логическим следствием формулы ψ, потому что...4. Формула ψ не является логическим следствием формулы ϕ, потому что...5. Все приведенные выше утверждения в общем случае неверны, потому что...Задача 10 (3 балла).

Пусть Γ — некоторое множество замкнутых формул логики предикатов. Верноли, что Γ является непротиворечивым множеством тогда и только тогда всякая дизъюнкция вида¬ϕ1 ∨¬ϕ1 ∨. . .∨¬ϕn , где ϕ1 , ϕ2 , . . . , ϕn — формулы из Γ, не является общезначимой. Варианты ответов:1. Верно, потому что ...2.

Неверно, потому что ...3. Зависит от множества Γ, и подтверждением тому служат два следующих примера ...Задача 10 (3 балла). Известно, что выполнимые замкнутые формулы ϕ и ψ не имеют ни однойобщей модели. Какие из приведенных ниже утверждений всегда верны и почему?1. Существует формула χ, логическим следствием которой являются обе формулы ϕ и ψ, потомучто ...2. Существует формула χ, являящаяся логическим следствием обеих формул ϕ и ψ, потому что ...3. Не существует ни одного успешного табличного вывода из семантической таблицы h{ϕ}, {ψ}i,потому что ...4. Все приведенные выше утверждения верны.Задача 11 (3 балла). Пусть задано некоторое непустое множество дизъюнктов S0 . Пусть S1 — этомножество всех формул, резолютивно выводимых из множества дизъюнктов S0 .