Сборник задач для самостоятельных занятий, страница 5
Описание файла
PDF-файл из архива "Сборник задач для самостоятельных занятий", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст 5 страницы из PDF
«Если среди граждан страны есть честные люди, то все политики — честные».2. «Если среди политиков найдется хоть один бесчестный человек, то во всем мире большене осталось честных людей».Упражнение 1.84. Рассмотрим ориентированный граф Γ с множеством вершин a, b, c, d, e имножеством дуг ha, bi, ha, ei, hb, ai, hd, bi, he, ci, he, ci, hc, di. Этот граф полностью определетсяследующим списком атомарных формул:ϕ1ϕ2ϕ3ϕ4ϕ5ϕ6======A(b, e),A(a, e),A(b, a),A(d, b),A(e, c),A(c, d).1.8. Метод резолюций в логике предикатовD1@@@D221Di@@D3@R@D00@RD0D39?DD0 — вариант D:Рис.
1.1.D3−i9?D0D = D0 θD0 = DηПереключательное свойство резолютивного выводаВершина v ориентированного графа считается достижимой из вершины u, если в этом графе существует ориентированный путь (маршрут) из вершины u в вершину v. Отношениедостижимости E (2) описывается следующими формулами:ψ1ψ2ψ3= ∀X E(X, X),= ∀X∀Y (A(X, Y ) → E(X, Y )),= ∀X∀Y ∀Z (E(X, Y ) & E(Y, Z) → E(X, Z)).1.
Сформулируйте в терминах логического следствия задачу проверки достижимости вграфе Γ вершины d из вершины a. Решите эту задачу при помощи метода резолюций.2. Ориентированный граф называется сильно связным, если для любой пары его вершинu, v вершина v достижима из вершины u. Сформулируйте в терминах логического следствия задачу проверки сильной связности графа Γ. Решите эту задачу при помощиметода резолюций.Упражнение 1.85. Граф называется двудольным, если множество всех его вершины можно разбить на два таких класса, что никакие две вершины из одного и того же класса несоединены дугой.1.
Введя вспомогательные предикаты, запишите формулу выражающую свойство двудольности графа.22Глава 1. УПРАЖНЕНИЯ2. Докажите при помощи метода резолюций, что граф Γ из упражнения 1.84 не являетсядвудольным.Упражнение 1.86. Граф называется 3-раскрашиваемым, если множество всех его вершиныможно разбить на три таких класса, что никакие две вершины из одного и того же класса несоединены дугой.1. Введя вспомогательные предикаты, запишите формулу выражающую свойство 3-раскрашиваемости графа.2. Докажите при помощи метода резолюций, что граф Γ не является 3-раскрашиваемым.1.9Полнота метода резолюцийУпражнение 1.87.
Пусть задано некоторое непустое множество дизъюнктов S0 . Пусть S1— это множество всех формул, резолютивно выводимых из множества дизъюнктов S0 . Какиеиз приведенных ниже утверждений всегда справедливы и почему?1. Если каждый дизъюнкт множества S0 выполним, то и каждый дизъюнкт множества S1выполним, потому что....2. Если каждый дизъюнкт множества S1 выполним, то множество дизъюнктов S0 имеетмодель, потому что....3.
Если множество дизъюнктов S0 имеет модель, то множество дизъюнктов S1 имеет модель, потому что....Упражнение 1.88. Останется ли верной теорема полноты резолютивного вывода в томслучае, если при построении вывода не пользоваться правилом склейки?Упражнение 1.89. Предположим, что в правило резолюции было внесено следующее изменение: резольвентой дизъюнктов D1 = D10 ∨L1 и D2 = D20 ∨¬L2 объявляется всякий дизъюнктD0 = (D10 ∨ D20 )η, где η — некоторый унификатор (необязательно наиболее общий) литер L1и L2 . Какие из приведенных ниже утверждений будут справедливы и почему?1.
После такого изменения и теорема корректности резолютивного вывода и теорема полноты резолютивного вывода уже будут неверны, потому что...2. После такого изменения теорема корректности резолютивного вывода остается верной,а теорема полноты резолютивного вывода уже будет неверна, потому что...3. После такого изменения теорема полноты резолютивного вывода остается верной, атеорема корректности резолютивного вывода уже будет неверна, потому что...4. После такого изменения и теорема корректности резолютивного вывода и теорема полноты резолютивного вывода остаются верными, потому что...1.9.
Полнота метода резолюций23Упражнение 1.90. Известно, что из множества непустых дизъюнктов S = {D1 , D2 , . . . , DN }можно построить резолютивный вывод пустого дизъюнкта . Какие из приведенных нижеутверждений всегда справедливы и почему?1. Существует успешный табличный вывод для исходной таблицы T = h∅, {D1 &D2 & . . . &DN }i,потому что. . . .2. Существует успешный табличный вывод для исходной таблицы T = h{D1 &D2 & . . .
&DN }, ∅i,потому что. . . .3. Существует успешный табличный вывод для исходной таблицы T = h∅, {D1 ∨ D2 ∨ · · · ∨DN }i, потому что. . . .4. Существует успешный табличный вывод для исходной таблицы T = h{D1 ∨ D2 ∨ · · · ∨DN }, ∅i, потому что. . . .Упражнение 1.91. Пусть S - это некоторое множество дизъюнктов, а [S] - это множествовсех основных примеров дизъюнктов из множества S. Какие из приведенных ниже утверждений всегда справедливы и почему?1. Если дизъюнкт D резолютивно выводим из множества дизъюнктов S, то этот же дизъюнкт D резолютивно выводим из множества основных примеров дизъюнктов [S], потомучто...2.
Если дизъюнкт D резолютивно выводим из множества основных примеров дизъюнктов[S], то этот же дизъюнкт D резолютивно выводим из множества дизъюнктов S, потомучто...3. Если эрбрановская интерпретация I является моделью для множества дизъюнктов S,то эта же эрбрановская интерпретация I является моделью для множества основныхпримеров дизъюнктов [S], потому что...4. Если эрбрановская интерпретация I является моделью для множества основных примеров дизъюнктов [S], то эта же эрбрановская интерпретация I является моделью длямножества дизъюнктов S, потому что...Упражнение 1.92.
Предположим, что из системы дизъюнктов S можно резолютивно вывести дизъюнкт P ∨ ¬P . Какие из приведенных ниже утверждений будут всегда верны ипочему?1. В системе дизъюнктов S есть противоречивый дизъюнкт, потому что. . .2. Система дизъюнктов S непротиворечива, потому что. . .3. Система дизъюнктов S противоречива, потому что. . .4. Такой резольвенты вывести из системы дизъюнктов S невозможно, потому что. . .24Глава 1.
УПРАЖНЕНИЯ1.10Хорновские логические программы. Декларативнаяи операционная семантики.Упражнение 1.93. Следующие основные свойства и отношения• мужчина(X),• женщина(Y ),• мать(X, Y ),• отец(X, Y ),• супруги(X, Y )описываются фактами хорновской логической программы, например,мужчина(adam)←;женщина(eve)←;отец(adam,abel)←;мать(eve,cain)←;Продолжите эту логическую программу, создав подходящие программные утверждения, описывающие следующие родственные свойства и отношения:1. родитель(X, Y );2. дед(X, Y );3. быть_отцом(X);4.
брат(X, Y );5. свояченица(X, Y );6. предок(X, Y );7. потомок(X, Y );8. родственник(X, Y );Упражнение 1.94. Создайте логические программы, описывающие следующие свойстватермов:list(X) — "Y является списком".elem(X, Y ) — "X является элементом списка Y ",Выяснить, каково множество правильных ответов на следующие запросы, обращенные к построенным программам:1. ? list(a.b.c.nil)1.10. Хорновские логические программы. Декларативная и операционная семантики.252. ? list(a.X.nil)3. ? list(a.b)4. ? list(a.Y)5. ? elem(b,a.b.c.nil)6. ? elem(X,a.b.c.nil)7. ? elem(a,X)Упражнение 1.95.
Постройте SLD-резолютивные вычисления для каждого из запросов,приведенных в упражнении 1.94, обращенных к программам, описывющим предикаты list иelem.Упражнение 1.96. Постройте всевозможные SLD-резолютивные вычисления для запросаG= ? R(Y),P(Z), обращенного к программе P, выделяя в каждом целевом утверждении самуюлевую подцель.
Каково множество вычисленных ответов на запрос G к программе P?P: R(Y) ← P(Y),Q(Y);P(a) ← ;P(b) ← ;Q(a) ← ;Q(f(X)) ← Q(X);Упражнение 1.97. Построить логические программы, описывающие следующие свойстваи отношения на множестве списков.1. head(L, X) : Заголовком списка L является элемент X;2. tail(L, X) : Хвостом списка L является список X;3.
pref ix(L, X) : Префиксом (начальным подсписком) списка L является список X;4. suf f ix(L, X) : Суффиксом (заключительным подсписком) списка L является список X;5. sublist(L, X) : Список X является подсписком списка L;6. equal(X, Y ) : Списки X и Y совпадают;7. equal_length(X, Y ) : Списки X и Y имеют одинаковую длину;8. nonequal_length(X, Y ) : Списки X и Y разную длину;9. less(X, Y ) : Длина списка X меньше длины списка Y ;10.