Семинарские занятия (Решения задач)
Описание файла
PDF-файл из архива "Семинарские занятия (Решения задач)", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 7 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Московский государственный университет имени М. В. ЛомоносоваФакультет вычислительной математики и кибернетикиКафедра системного программированияРешение задач по курсу математической логикиМосква, 2009by kayrickСодержание1 Формулы логики предикатов22 Вывод семантических таблиц33 Нормальные формы и унификация3.1 Приведение к ССФ .
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3.2 Нахождение НОУ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3.3 Задачи . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . . . . . . . . . .111111114 Метод резолюций155 Хорновские логические программы. Декларативные и операционные семантики.206 Встроенные функции и предикаты297 Операторы отсечения и отрицания318 Экзаменационные задачи3611Формулы логики предикатовУпражнение 1.11. Σ = {L2 }L(x, y) − x любит y∀x L(x, x)&(∀x L(x, x)2.
Σ = {P 1 , M 1 , S 1 , C 2 , a, b}→∃y ∃z L(y, z))P (x)−M (x)−S(x)− C(x, y) −− ab−x - задачаx - математикзадача x - разрешимаматематик x может решить задача y константа «Я»константа «эта задача»(∀x(P (x)&S(x) → ∃y(M (y) & C(y, x)))) & (M (a)&¬C(a, b)) → ¬S(b)C(x, y, t) − x может обмануть y в момент времени t33. Σ = {C , a}a− Константа «Вы»(∃t ∀x C(a, x, t)) & (∃x ∀t (Ca, x, t)) & ¬(∀x ∀t C(a, x, t))Упражнение 1.21. ∃x (∀y (B(y) & C(y) & U (x, y))) & S(x)2. ∀x ∀y (B(x) & S(x) & W (y) & C(y) → ¬U (y, x))3. ∀x (B(x) → (S(x) &(∀y (W (y) & C(y) → U (y, x)))) ∨ (C(x) & (∃ y (S(y) & U (x, y)))))4.
∀x ∀y (B(x) & C(x) & W (y) & S(y) → ¬(U (x, y) ∨ U (y, x)))5. (∀x (S(x) → B(x))) → (∀y (C(y) → ¬W (y)))6. ∀x (¬(C(x) & W (x) & (∃z (S(z) & U (x, z)))) → B(x) & (∀z (W (x) → U (z, x))))Упражнение 1.31. ∀x ∀y (P (x) & P (y) & ¬E(x, y) →∃k (L(k) & B(x, k) & B(y, k) & (∀s (L(s) & B(x, s) & B(y, s) → E(k, s)))))2. ∀i (P (i) & L(x) & L(y) & B(i, x) → ¬B(i, y))[= P ar(x, y)]3. ∀x (L(x) → ∀y (P (y) & ¬B(y, x) → ∃k (L(k) & B(y, k) &P ar(x, k) & ∀s (L(s) & B(y, s) & P ar(x, s) → E(k, s)))))Упражнение 1.41. Z(x) = ∀y S(y, x, y)2.
O(x) = ∀y P (y, x, y)3. T (x) = ∃k ∀y (P (y, k, y) & S(k, k, x))4. ∃y (Z(y) & S(x, y, n))5. ∃y ∃z (T (y) & P (z, y, x))6. (∀k ∀l (P (k, l, x) → (O(k) ∨ O(l)))) & ¬(O(x) ∨ Z(x)))1. E(x, y) = ∃k ((∀y S(y, k, y)) & S(x, k, y))2. L(x, y) = ∃k ((∃x ¬S(k, x, k)) & S(x, k, y))3. F (x, y) = ∃k P (y, k, x)22Вывод семантических таблицУпражнение 2.11. ∃x P (x) & ∃x ¬ P (x)• ВыполнимаDI = {0, 1}, P(0) = true, P(1) = false• Не общезначимаDI = {0}, P(0) = true2. ∃x P (x) ∨ ∃x ¬ P (x)• Общезначимаh∅ | ∃x P (x) ∨ ∃x ¬ P (x)iyR∨h∅ | ∃x P (x), ∃x ¬ P (x)iyR∃h∅ | ∃x P (x), ∃x ¬ P (x), P (c1 )iyR∃h∅ | ∃x P (x), ∃x ¬ P (x), P (c1 ), ¬P (c1 )iyR¬DEP (c1 ) | ∃x P (x), ∃x ¬ P (x), P (c1 )Закрытая таблица3.
∃x ∀y (P (x) & ¬P (y))• НевыполнимаДокажем невыполнимость путем доказательства общезначимости отрицанияh∃x ∀y (P (x) & ¬P (y))|∅iyL∃h∀y (P (c1 ) & ¬P (y))|∅iyL∀h∀y (P (c1 ) & ¬P (y)), P (c1 ) & ¬P (c1 )|∅iyL&h∀y (P (c1 ) & ¬P (y)), P (c1 ), ¬P (c1 )|∅iyL¬ED∀y (P (c1 ) & ¬P (y)), P (c1 )|P (c1 )Закрытая таблица4. P (x) → ∀x P (x)• ВыполнимаDI = {0}, P(0) = true• Не общезначимаDI = {0, 1}, P(0) = true, P(1) = false5. ∀x P (x) → P (x)3• Общезначима (очевидно)6.
∀y ∃x R(x, y) → ∃x ∀y R(x, y)• ВыполнимаDI = {0}, R(0, 0) = true• Не общезначимаDI = N, R(x, y) = x > y7. (∀x P (x) → ∀x Q(x)) → ∀x (P (x) → Q(x))• ВыполнимаDI = N, P(x) = Q(x)• Не общезначимаDI = N, P(x) = (x mod 2 == 0), Q(x) = (x mod 4 == 0)Упражнение 2.21. ∃x P (x) → ¬∀x ¬P (x)Tφ = h∅ | ∃x P (x) → ¬∀x ¬P (x)iR→∨T1 = h∃x P (x) | ¬∀x ¬P (x)iL∃∨T2 = hP (c1 ) | ¬∀x ¬P (x)iR¬∨T3 = hP (c1 ), ∀x ¬P (x) | ∅iL∀∨T4 = hP (c1 ), ∀x ¬P (x), ¬P (c1 ) | ∅i∨L¬DT5 = P (c1 ), ∀x ¬P (x) | P (c1 )Закрытая таблицаE2. ∃x∀y R(x, y) → ∀y∃x R(x, y)Tφ = h∅ | ∃x∀y R(x, y) → ∀y∃x R(x, y)iR→∨Tφ = h∃x∀y R(x, y) | ∀y∃x R(x, y)iL∃∨Tφ = h∀y R(c1 , y) | ∀y∃x R(x, y)iR∀∨Tφ = h∀y R(c1 , y) | ∃x R(x, c2 )iR∃∨Tφ = h∀y R(c1 , y) | ∃x R(x, c2 ), R(c1 , c2 )iL∀∨DETφ = ∀y R(c1 , y) , R(c1 , c2 )| ∃x R(x, c2 ), R(c1 , c2 )4Закрытая таблица3.
∀x (P (x) → ∃y R(x, f (y))) → (∃x ¬P (x) ∨ ∀x∃z R(x, z))Tφ = h∅ | ∀x (P (x) → ∃y R(x, f (y))) → (∃x ¬P (x) ∨ ∀x∃z R(x, z))iR→∨T1 = h∀x (P (x) → ∃y R(x, f (y))) | ∃x ¬P (x) ∨ ∀x∃z R(x, z)iR∨∨T2 = h∀x (P (x) → ∃y R(x, f (y))) | ∃x ¬P (x), ∀x∃z R(x, z)iR∀∨T3 = h∀x (P (x) → ∃y R(x, f (y))) | ∃x ¬P (x), ∃z R(c1 , z)i∨ L∀φ1*+z}|{T4 = ∀x (P (x) → ∃y R(x, f (y))), P (c1 ) → ∃y R(c1 , f (y)) | ∃x ¬P (x), ∃z R(c1 , z)L→L→∨∨T4.1 = hφ1 , ∃y R(c1 , f (y)) | ∃x ¬P (x), ∃z R(c1 , z)iT4.2 = hφ1 , | ∃x ¬P (x), ∃z R(c1 , z), P (c1 )iR∃L∃∨∨T5.1 = hφ1 , R(c1 , f (c2 )) | ∃x ¬P (x), ∃z R(c1 , z)iR∃T5.2 = hφ1 , | ∃x ¬P (x), ∃z R(c1 , z), P (c1 ), ¬P (c1 )i∨∨DT5.1 = φ1 , R(c1 , f (c2 )) | ∃x ¬P (x), ∃z R(c1 , z), R(c1 , f (c2 ))Закрытые таблицыER6DET5.2 = φ1 , P (c1 ) | ∃x ¬P (x), ∃z R(c1 , z), P (c1 )4.
∀x∃y∀z(P (x, y) → P (y, z))Tφ = h∅ | ∀x∃y∀z(P (x, y) → P (y, z))iR∀∨T1 = h∅ | ∃y∀z(P (c1 , y) → P (y, z))iR∃∨T2 = h∅ | ∃y∀z(P (c1 , y) → P (y, z)), ∀z(P (c1 , c1 ) → P (c1 , z))iR∀∨T3 = h∅ | ∃y∀z(P (c1 , y) → P (y, z)), P (c1 , c1 ) → P (c1 , c2 )iR→∨T4 = hP (c1 , c1 ) | ∃y∀z(P (c1 , y) → P (y, z)), P (c1 , c2 )iR∃∨T5 = hP (c1 , c1 ) | ∃y∀z(P (c1 , y) → P (y, z)), P (c1 , c2 ), ∀z(P (c1 , c2 ) → P (c2 , z))iR∀∨T6 = hP (c1 , c1 ) | ∃y∀z(P (c1 , y) → P (y, z)), P (c1 , c2 ), P (c1 , c2 ) → P (c2 , c3 )i∨R→DET7 = P (c1 , c1 ), P (c1 , c2 )| ∃y∀z(P (c1 , y) → P (y, z)), P (c1 , c2 ), P (c2 , c3 )5Закрытая таблица5.
∃x∀y∃z(P (x, y) → P (y, z))*+∅ | ∃x∀y∃z(P (x, y) → P (y, z))|{z}Tφ =φ1R∃∨T1 = h∅ | φ1 , ∀y∃z(P (c1 , y) → P (y, z))iR∀ ∨*T2 =+∅ | φ1 , ∃z(P (c1 , c2 ) → P (c2 , z))|{z}φ2R∃∨T3 = h∅ | φ1 , φ2 , P (c1 , c2 ) → P (c2 , c1 ), P (c1 , c2 ) → P (c2 , c2 )iR→∨T4 = hP (c1 , c2 ) | φ1 , φ2 , P (c2 , c1 ), P (c2 , c2 )i(φ1 )R∃∨T5 = hP (c1 , c2 ) | φ1 , φ2 , P (c2 , c1 ), P (c2 , c2 ), ∀y∃z(P (c2 , y) → P (y, z))iR∀ ∨*T6 =+P (c1 , c2 ) | φ1 , φ2 , P (c2 , c1 ), P (c2 , c2 ), ∃z(P (c2 , c3 ) → P (c3 , z))|{z}φ3R∃∨T7 = hP (c1 , c2 ) | φ1 , φ2 , φ3 , P (c2 , c1 ), P (c2 , c2 ), P (c2 , c3 ) → P (c3 , c3 )iR→∨T8 = hP (c1 , c2 ), P (c2 , c3 ) | φ1 , φ2 , φ3 , P (c2 , c1 ), P (c2 , c2 ), P (c3 , c3 )i(φ2 )R∃∨T9 = hP (c1 , c2 ), P (c2 , c3 ) | φ1 , φ2 , φ3 , P (c2 , c1 ), P (c2 , c2 ), P (c3 , c3 ), P (c1 , c2 ) → P (c2 , c3 )iR→∨DET10 = P (c1 , c2 ), P (c2 , c3 ) | φ1 , φ2 , φ3 , P (c2 , c1 ), P (c2 , c2 ), P (c3 , c3 ), P (c2 , c3 )Закрытая таблица6.
∀x (P (x) & R(x)) → (∀x P (x) & ∀x R(x))6Tφ = h∅ | ∀x (P (x) & R(x)) → (∀x P (x) & ∀x R(x))iR→∨T1 = h∀x (P (x) & R(x)) | ∀x P (x) & ∀x R(x)iR&R&∨∨T2.1 = h∀x (P (x) & R(x)) | ∀x R(x)iT2.2 = h∀x (P (x) & R(x)) | ∀x P (x)iR∀R∀∨∨T2.1 = h∀x (P (x) & R(x)) | R(c1 )iT2.2 = h∀x (P (x) & R(x)) | P (c1 )iL∀L∀∨∨T3.1 = h∀x (P (x) & R(x)), P (c1 ) & R(c1 ) | R(c1 )iT3.2 = h∀x (P (x) & R(x)), P (c1 ) & R(c1 ) | P (c1 )iL&L&∨DET3.1 = ∀x (P (x) & R(x)), P (c1 ), R(c1 ) | R(c1 )Закрытые таблицыT3.2∨DE= ∀x (P (x) & R(x)), P (c1 ), R(c1 ) | P (c1 )7.
(∀x P (x) & ∀x R(x)) → ∀x (P (x) & R(x))Tφ = h∅ | (∀x P (x) & ∀x R(x)) → ∀x (P (x) & R(x))iR→∨T1 = h∀x P (x) & ∀x R(x)) | ∀x (P (x) & R(x))iL&∨T2 = h∀x P (x), ∀x R(x)) | ∀x (P (x) & R(x))iR∀∨T3 = h∀x P (x), ∀x R(x)) | P (c1 ) & R(c1 )iL∀∨T4 = h∀x P (x), ∀x R(x), P (c1 ), R(c1 ) | P (c1 ) & R(c1 )i∨R&DT4.1 = ∀x P (x), ∀x R(x), P (c1 ), R(c1 ) | R(c1 )Закрытые таблицыR&ET4.28. ∃x (P (x) ∨ R(x)) → (∃x P (x) ∨ ∃x R(x))7∨DE= ∀x P (x), ∀x R(x), P (c1 ), R(c1 ) | P (c1 )Tφ = h∅ |∃x (P (x) ∨ R(x)) → (∃x P (x) ∨ ∃x R(x)) iR→∨T1 = h∃x (P (x) ∨ R(x)) | ∃x P (x) ∨ ∃x R(x) iL∃∨T2 = hP (c1 ) ∨ R(c1 ) | ∃x P (x) ∨ ∃x R(x) iR∨∨T3 = hP (c1 ) ∨ R(c1 ) | ∃x P (x), ∃x R(x) iR∃∨T4 = hP (c1 ) ∨ R(c1 ) | ∃x P (x), ∃x R(x), P (c1 ), R(c1 ) i∨L∨DT5.1 = R(c1 ) | ∃x P (x), ∃x R(x), P (c1 ), R(c1 )Закрытые таблицы∨ET5.2L∨DE= P (c1 ) | ∃x P (x), ∃x R(x), P (c1 ), R(c1 )9.
(∃x P (x) ∨ ∃x R(x)) → ∃x (P (x) ∨ R(x))Tφ = h∅ | (∃x (P (x) ∨ ∃x R(x)) → ∃x (P (x) ∨ R(x))iR→∨T1 = h∃x (P (x) ∨ ∃x R(x) | ∃x (P (x) ∨ R(x))iL∨L∨∨∨T2.1 = h∃x R(x) | ∃x (P (x) ∨ R(x))iT2.2 = h∃x P (x) | ∃x (P (x) ∨ R(x))iL∃L∃∨∨T3.1 = hR(c1 ) | ∃x (P (x) ∨ R(x))iT3.2 = hP (c1 ) | ∃x (P (x) ∨ R(x))iR∃R∃∨∨T4.1 = hR(c1 ) | ∃x (P (x) ∨ R(x)), P (c1 ) ∨ R(c1 )iT4.2 = hP (c1 ) | ∃x (P (x) ∨ R(x)), P (c1 ) ∨ R(c1 )iR∨∨EDT5.1 = R(c1 ) | ∃x (P (x) ∨ R(x)), P (c1 ), R(c1 )Закрытые таблицы10. (∀x P (x) ∨ R(y)) → ∀x (P (x) ∨ R(y))8R∨T5.2∨DE= P (c1 ) | ∃x (P (x) ∨ R(x)), P (c1 ), R(c1 )Tφ = h∅ | (∀x P (x) ∨ R(y)) → ∀x (P (x) ∨ R(y))iR→∨T1 = h∀x P (x) ∨ R(y) | ∀x (P (x) ∨ R(y))iR∀∨T2 = h∀x P (x) ∨ R(y) | P (c1 ) ∨ R(y)iR∨∨T3 = h∀x P (x) ∨ R(y) | P (c1 ), R(y)i∨R∨∨T4.1 = h∀x P (x) | P (c1 ), R(y)iR∨ET4.2 = R(y) | P (c1 ), R(y)DR∀∨DET5.1 = ∀x P (x), P (c1 )| P (c1 ), R(y)Закрытые таблицы11.
∀x (P (x) ∨ R(y)) → (∀x P (x) ∨ R(y))Tφ = h∅ | ∀x (P (x) ∨ R(y)) → (∀x P (x) ∨ R(y))iR→∨T1 = h∀x (P (x) ∨ R(y)) | (∀x P (x) ∨ R(y))iR∨∨T2 = h∀x (P (x) ∨ R(y)) | ∀x P (x), R(y)iR∀∨T3 = h∀x (P (x) ∨ R(y)) | P (c1 ), R(y))iL∀∨T4 = h∀x (P (x) ∨ R(y)), P (c1 ) ∨ R(y) | P (c1 ), R(y))i∨DR∨ET5.1 = ∀x (P (x) ∨ R(y)), P (c1 ) | P (c1 ), R(y)Закрытые таблицы∨R∨DT5.2 = ∀x (P (x) ∨ R(y)), R(y) | P (c1 ), R(y)12.
∃y∀x Q(x, y) → ∀x∃y Q(x, y)9ETφ = h∅ | ∃y∀x Q(x, y) → ∀x∃y Q(x, y)iR→∨T1 = h∃y∀x Q(x, y) | ∀x∃y Q(x, y)iR∀∨T2 = h∃y∀x Q(x, y) | ∃y Q(c1 , y)iL∃∨T3 = h∀x Q(x, c2 ) | ∃y Q(c1 , y)iL∀∨T4 = h∀x Q(x, c2 ), Q(c1 , c2 ) | ∃y Q(c1 , y)iR∃∨DET4 = ∀x Q(x, c2 ), Q(c1 , c2 ) | ∃y Q(c1 , y), Q(c1 , c2 )Закрытая таблицаУпражнение 2.31. ∀x (P (x) ∨ Q(x)) → (∀x P (x) ∨ ∀x Q(x))Вывод не будет успешным так как формула не общезначима.DI = N, P(x) = (x mod 2 == 0), Q(x) = (x mod 2 == 1)2. ∃x (P (x) ∨ Q(x)) → (∃x P (x) ∨ ∃x Q(x))Построим выводh∅|∃x (P (x) ∨ Q(x)) → (∃x P (x) ∨ ∃x Q(x))iR→∨h∃x (P (x) ∨ Q(x))|∃x P (x) ∨ ∃x Q(x)i∃∨hP (c1 ) ∨ Q(c1 )|∃x P (x) ∨ ∃x Q(x)iR∨∨hP (c1 ) ∨ Q(c1 )|∃x P (x), ∃x Q(x)iR∃∨hP (c1 ) ∨ Q(c1 )|∃x P (x), ∃x Q(x), P (c1 ), Q(c1 )iL∨D∨ ∨L∨EDEP (c1 )|∃x P (x), ∃x Q(x), P (c1 ), Q(c1 ) Q(c1 )|∃x P (x), ∃x Q(x), P (c1 ), Q(c1 )Упражнение 2.4 Пусть такая формула существует.
Рассмотрим ее на интерпретации, область которойсодержит три элемента. На данной интерпретации формула истинна. То есть для любой подстановки онаистинна. Следовательно существует подстановка, состоящая из 1 или 2 объектов, на которой формула также истинна. Следовательно формула истинна на интерпретации, область которой содержит только эти2 объекта, следовательно такой формулы нет.Упражнение 2.5∃x1 ∃x2 ∃x3 ∃x4 ∃x5&yi ∈{x1 ,x2 ,x3 ,x4 ,x5 }P (y1 , y2 , y3 , y4 , y5 )→ ∀x1 ∀x2 ∀x3 ∀x4 ∀x5 P (x1 , x2 , x3 , x4 , x5 )103Нормальные формы и унификация3.1Приведение к ССФ1.