Редактирование: Математическая Логика, решение задач/variant 2004

Материал из eSyr's wiki.

Перейти к: навигация, поиск

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

Текущая версия Ваш текст
Строка 20: Строка 20:
&phi;<sub>3</sub> = &exist; p (A(p, y) &amp; ((a &le; p) &amp; (p &le; b)))
&phi;<sub>3</sub> = &exist; p (A(p, y) &amp; ((a &le; p) &amp; (p &le; b)))
-
&forall; a &forall; b &forall; y (S(y) &amp; &phi;<sub>1</sub> &amp; &phi;<sub>2</sub> &amp; (S(y) &amp; &phi;<sub>1</sub> &amp; &phi;<sub>2</sub> &rarr; &phi;<sub>3</sub>))
+
&forall; a &forall; b &forall; y (S(y) &amp; &phi;<sub>1</sub> &amp; &phi;<sub>2</sub> &amp; (S(y) &amp; &phi;<sub>1</sub> &amp; &phi;<sub>2</sub> &rarr; &phi;<sub>4</sub>))
=== Задача 2 ===
=== Задача 2 ===
Строка 47: Строка 47:
''Каковы бы ни были две последовательности действительных чисел такие, что первая одна из них &rarr; 0, а другая ограничена, тогда из произведение тоже &rarr; 0.''
''Каковы бы ни были две последовательности действительных чисел такие, что первая одна из них &rarr; 0, а другая ограничена, тогда из произведение тоже &rarr; 0.''
-
&phi;<sub>1</sub> = &exist; M (R(M) &amp; &forall; n (N(n) &amp; &exist; x (R(x) &amp; E(x, n, y) &amp; (|x| &lt; M))))
+
&phi;<sub>1</sub> = &forall; n (N(n) &amp; &exist; x &exist; M (R(M) &amp; R(x) &amp; E(x, n, y) &amp; (x &lt; M)))
&phi;<sub>2</sub> = &exist; y<sub>3</sub> (S(y<sub>3</sub>) &amp; &forall; n (N(n) &exist; x<sub>1</sub> &exist; x<sub>2</sub> &exist; x<sub>3</sub> (E(x<sub>1</sub>, n, y<sub>1</sub>) &amp; E(x<sub>2</sub>, n, y<sub>2</sub>) &amp; E(x<sub>3</sub>, n, y<sub>3</sub>) &amp; (x<sub>3</sub> = x<sub>1</sub> &times; x<sub>2</sub>))))
&phi;<sub>2</sub> = &exist; y<sub>3</sub> (S(y<sub>3</sub>) &amp; &forall; n (N(n) &exist; x<sub>1</sub> &exist; x<sub>2</sub> &exist; x<sub>3</sub> (E(x<sub>1</sub>, n, y<sub>1</sub>) &amp; E(x<sub>2</sub>, n, y<sub>2</sub>) &amp; E(x<sub>3</sub>, n, y<sub>3</sub>) &amp; (x<sub>3</sub> = x<sub>1</sub> &times; x<sub>2</sub>))))
Строка 55: Строка 55:
''Нет такой сходящейся последовательности, что ее нельзя было бы представить как сумму двух сходящихся последовательностей.''
''Нет такой сходящейся последовательности, что ее нельзя было бы представить как сумму двух сходящихся последовательностей.''
-
&phi;<sub>1</sub>(y) = S(y) &amp; &exist; m (R(m) &amp; M(m, y))
+
&phi;<sub>1</sub>(y) = S(y) &amp; &exist; m (R(m) &amp; (m, y))
-
&phi;<sub>2</sub>(y<sub>1</sub>, y<sub>2</sub>, y<sub>3</sub>) = (S(y<sub>3</sub>) &amp; &forall; n (N(n) &exist; x<sub>1</sub> &exist; x<sub>2</sub> &exist; x<sub>3</sub> (E(x<sub>1</sub>, n, y<sub>1</sub>) &amp; E(x<sub>2</sub>, n, y<sub>2</sub>) &amp; E(x<sub>3</sub>, n, y<sub>3</sub>) &amp; (x<sub>3</sub> = x<sub>1</sub> + x<sub>2</sub>))))
+
&phi;<sub>2</sub>(y<sub>1</sub>, y<sub>2</sub>, y<sub>3</sub>) = (S(y<sub>3</sub>) &amp; &forall; n (N(n) &exist; x<sub>1</sub> &exist; x<sub>2</sub> &exist; x<sub>3</sub> (E(x<sub>1</sub>, n, y<sub>1</sub>) &amp; E(x<sub>2</sub>, n, y<sub>2</sub>) &amp; E(x<sub>3</sub>, n, y<sub>3</sub>) &amp; (x<sub>3</sub> = x<sub>1</sub> &times; x<sub>2</sub>))))
-
&not;(&exist; y<sub>3</sub> (&phi;<sub>1</sub>(y) &amp; &forall; y<sub>1</sub> &forall; y<sub>2</sub> (&phi;<sub>1</sub>(y<sub>1</sub>) &amp; &phi;<sub>1</sub>(y<sub>2</sub>) &amp; &not;&phi;<sub>2</sub>(y<sub>1</sub>, y<sub>2</sub>, y<sub>3</sub>))))
+
&not;(&exist; y (&phi;<sub>1</sub>(y) &amp; &forall; y<sub>1</sub> &forall; y<sub>2</sub> (&phi;<sub>1</sub>(y<sub>1</sub>) &amp; &phi;<sub>1</sub>(y<sub>2</sub>) &amp; &not;&phi;<sub>2</sub>(y<sub>1</sub>, y<sub>2</sub>, y))))
== Табличный вывод ==
== Табличный вывод ==
=== Правила ===
=== Правила ===
-
# <math>L\neg:\frac{<\neg\phi,\Gamma|\Delta>}{<\Gamma|\phi,\Delta>}</math>
+
# <math>L\neg:\frac{<\phi,\Gamma|\Delta>}{<\Gamma|\phi,\Delta>}</math>
# <math>R\neg:\frac{<\Gamma|\neg\phi,\Delta>}{<\phi,\Gamma|\Delta>}</math>
# <math>R\neg:\frac{<\Gamma|\neg\phi,\Delta>}{<\phi,\Gamma|\Delta>}</math>
# <math>L\and:\frac{<\phi_1\and\phi_2,\Gamma|\Delta>}{<\phi_1,\phi_2,\Gamma|\Delta>}</math>
# <math>L\and:\frac{<\phi_1\and\phi_2,\Gamma|\Delta>}{<\phi_1,\phi_2,\Gamma|\Delta>}</math>
Строка 68: Строка 68:
# <math>L\lor:\frac{<\phi_1\lor\phi_2,\Gamma|\Delta>}{<\phi_1,\Gamma|\Delta><\phi_2,\Gamma|\Delta>}</math>
# <math>L\lor:\frac{<\phi_1\lor\phi_2,\Gamma|\Delta>}{<\phi_1,\Gamma|\Delta><\phi_2,\Gamma|\Delta>}</math>
# <math>R\lor:\frac{<\Gamma|\phi_1\lor\phi_2,\Delta>}{<\Gamma|\phi_1,\phi_2,\Delta>}</math>
# <math>R\lor:\frac{<\Gamma|\phi_1\lor\phi_2,\Delta>}{<\Gamma|\phi_1,\phi_2,\Delta>}</math>
-
# <math>L\to:\frac{<\phi_1\to\phi_2,\Gamma|\Delta>}{<\phi_2,\Gamma|\Delta><\Gamma|\phi_1,\Delta>}</math>
+
# <math>L\to:\frac{<\phi_1\to\phi_2,\Gamma|\Delta>}{<\phi_2,\Gamma|\phi_1,\Delta>}</math>
# <math>R\to:\frac{<\Gamma|\phi_1\to\phi_2,\Delta>}{<\phi_1,\Gamma|\phi_2,\Delta>}</math>
# <math>R\to:\frac{<\Gamma|\phi_1\to\phi_2,\Delta>}{<\phi_1,\Gamma|\phi_2,\Delta>}</math>
Строка 99: Строка 99:
<\forall{x}\forall{y}(P(x)\to R(y)),\forall{y}(P(t_1)\to R(y)),(P(t_1)\to R(t_2)),P(c_2)|R(c_1)> \\
<\forall{x}\forall{y}(P(x)\to R(y)),\forall{y}(P(t_1)\to R(y)),(P(t_1)\to R(t_2)),P(c_2)|R(c_1)> \\
\darr L\to \\
\darr L\to \\
-
<\forall{x}\forall{y}(P(x)\to R(y)),\forall{y}(P(t_1)\to R(y)),R(t_2),P(c_2)|R(c_1)>, <\forall{x}\forall{y}(P(x)\to R(y)),\forall{y}(P(t_1)\to R(y)),P(c_2)|P(t_1),R(c_1)> \\
+
<\forall{x}\forall{y}(P(x)\to R(y)),\forall{y}(P(t_1)\to R(y)),R(t_2),P(c_2)|P(t_1),R(c_1)> \\
\end{array}</math>
\end{array}</math>
-
Вторая таблица открыта, следовательно, формула не общезначима. (А разве нельзя провести унификацию терма t_2 = c_1, а t_1 = c_2?)
+
Пересечение &Gamma; и &Delta; непусто (при t<sub>1</sub> = c<sub>2</sub> или t<sub>2</sub> = c<sub>1</sub>). Получили закрытую таблицу, следовательно, формула общезначима.
 +
 
=== Задача 2 ===
=== Задача 2 ===
Строка 111: Строка 112:
'''Решение.'''
'''Решение.'''
-
<math>\begin{array}{c}\begin{array}{ccc}
+
<math>\begin{array}{ccc}
-
& <\empty|(\exist{y}P(y)\to\forall{x}R(x))\to\forall{x}\forall{y}(P(x)\to R(y))> \\
+
<\empty|(\exist{y}P(y)\to\forall{x}R(x))\to\forall{x}\forall{y}(P(x)\to R(y))> \\
-
& \darr R\to \\
+
\darr R\to \\
-
& <(\exist{y}P(y)\to\forall{x}R(x))|\forall{x}\forall{y}(P(x)\to R(y))> \\
+
<(\exist{y}P(y)\to\forall{x}R(x))|\forall{x}\forall{y}(P(x)\to R(y))> \\
-
& \darr L\to \\
+
\darr L\to \\
-
<\forall{x}R(x)|\exist{y}P(y),\forall{x}\forall{y}(P(x)\to R(y))> & & <\empty|\exist{y}P(y),\forall{x}\forall{y}(P(x)\to R(y))> \\
+
<\forall{x}R(x)|\exist{y}P(y),\forall{x}\forall{y}(P(x)\to R(y))> \\
-
\darr L\forall & & \darr R\exist \\
+
\darr L\to \\
-
<\forall{x}R(x),R(t_1)|\forall{x}\forall{y}(P(x)\to R(y))> & & <\empty|\exist{y}P(y),P(t_2),\forall{x}\forall{y}(P(x)\to R(y))> \\
+
<\forall{x}R(x)|\exist{y}P(y),\forall{x}\forall{y}(P(x)\to R(y))> \\
-
\darr R\forall & & \darr R\forall \\
+
\darr L\forall \\
-
<\forall{x}R(x),R(t_1)|\forall{y}(P(c_1)\to R(y))> & & <\empty|\exist{y}P(y),P(t_2),\forall{y}(P(c_2)\to R(y))> \\
+
<\forall{x}R(x),R(t_1)|\exist{y}P(y),\forall{x}\forall{y}(P(x)\to R(y))> \\
-
\darr R\forall & & \darr R\forall \\
+
\darr R\exist \\
-
<\forall{x}R(x),R(t_1)|(P(c_1)\to R(c_3))> & & <\empty|\exist{y}P(y),P(t_2),P(c_2)\to R(c_4)> \\
+
<\forall{x}R(x),R(t_1)|\exist{y}P(y),P(t_2),\forall{x}\forall{y}(P(x)\to R(y))> \\
-
\darr R\to & & \darr R\to \\
+
\darr R\forall \\
-
<\forall{x}R(x),R(t_1),P(c_1)|R(c_3)> & & <P(c_2)|\exist{y}P(y),P(t_2),R(c_4)> \\
+
<\forall{x}R(x),R(t_1)|\exist{y}P(y),P(t_2),\forall{y}(P(c_1)\to R(y))> \\
-
\end{array}\end{array}</math>
+
\darr R\forall \\
-
 
+
<\forall{x}R(x),R(t_1)|\exist{y}P(y),P(t_2),(P(c_1)\to R(c_2))> \\
-
Вторая таблица открыта, следовательно, формула не общезначима. (Аналогично унифицировав t_1 = c_3 и t_2 = c_2 мы получим закрытую таблицу).
+
\darr R\to \\
-
 
+
<\forall{x}R(x),R(t_1),P(c_1)|\exist{y}P(y),P(t_2),R(c_2)> \\
-
== Метод резолюций ==
+
-
 
+
-
=== Задача 1 ===
+
-
С помощью метода резолюций исследовать на противоречивость систему дизъюнктов S.
+
-
 
+
-
<math>\begin{cases}
+
-
D_1 = P(y_1, z_1)\lor\neg R(x_1, b) \\
+
-
D_2 = \neg Q(b, x_2)\lor\neg P(z_2, y_2) \\
+
-
D_3 = R(c, x_3)\lor P(x_3, g(y_3)) \\
+
-
D_4 = Q(y_4, y_4)\lor\neg P(x_4, g(y_4)) \\
+
-
D_5 = \neg P(x_5, y_5)\lor Q(f(x_5), y_5)
+
-
\end{cases}</math>
+
-
 
+
-
'''Решение.'''
+
-
 
+
-
(2)и(((1)и(5))и(3)) склеить в !(z2, g(b)), (1)и(3) склеить в P(b, g(b)).
+
-
<math>\begin{array}{l}
+
-
D^'_1 - D_1, D_5: R(x_1, b)\lor Q(f(x_5), x_5) \\
+
-
D^'_2 - D^'_1, D_3: P(b, g(y_3))\lor Q(f(x_5), x_5) \\
+
-
D^'_3 - D_2, D_4: \neg P(z_2, y_2) \lor \neg P(x_4, g(y_4)) \\
+
-
D^'_4 - D^'_3: \neg P(z_2, y_2) \\
+
-
D^'_5 - D_1, D_3: P(b, y_3)\lor P(y_1, z_1) \\
+
-
D^'_6 - D_1, D_3: P(b, y_3) \\
+
-
D^'_7 - D^'_4, D^'_6: []
+
\end{array}</math>
\end{array}</math>
 +
 +
Пересечение &Gamma; и &Delta; непусто (при t<sub>1</sub> = c<sub>2</sub> или t<sub>2</sub> = c<sub>1</sub>). Получили закрытую таблицу, следовательно, формула общезначима.
{{Курс Математическая Логика}}
{{Курс Математическая Логика}}

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Шаблоны, использованные на этой странице:

Разделы