Булевые формулы с кванторами как игры для двух игроков — различия между версиями
Ponomarev (обсуждение | вклад) |
м (rollbackEdits.php mass rollback) |
||
(не показано 12 промежуточных версий 3 участников) | |||
Строка 1: | Строка 1: | ||
− | + | {{Определение | |
− | + | |definition = В игре участвуют два игрока {{---}} «для всех» и «существует». Есть утверждение <tex>\exists x_1 \forall x_2 \exists x_3 \dots Q x_n \Psi(x_1,\dots ,x_n)\,</tex>. Игроки поочередно выбирают значения параметров. Каждый игрок выбирает значение в зависимости от предыдущих ходов. Цель игрока «существует» делать такие ходы, чтобы утверждение <tex>\exists x_1 \forall x_2 \exists x_3 \dots Q x_n \Psi(x_1,\dots ,x_n)\,</tex> получилось истинным. А цель игрока «для всех» делать такие ходы, чтобы итоговое выражение получилась ложным. | |
+ | }} | ||
+ | </noinclude> | ||
+ | <includeonly>{{#if:{{{id|}}}|<span id="{{{id}}}"></span>|}}{{#if: {{{neat|}}}| | ||
+ | <div style="background-color: #fcfcfc; float:left;"> | ||
+ | <div style="background-color: #ddd;">'''Определение:'''</div> | ||
+ | <div style="border:1px dashed #2f6fab; padding: 8px;">{{{definition}}}</div> | ||
+ | </div>| | ||
+ | <table border="0" width="100%"> | ||
+ | <tr><td style="background-color: #ddd">'''Определение:'''</td></tr> | ||
+ | <tr><td style="border:1px dashed #2f6fab; padding: 8px; background-color: #fcfcfc;">{{{definition}}}</td></tr> | ||
+ | </table>}} | ||
+ | </includeonly> | ||
==Интерпретация булевых формул с кванторами как игр для двух игроков== | ==Интерпретация булевых формул с кванторами как игр для двух игроков== | ||
{{Теорема | {{Теорема | ||
|statement= | |statement= | ||
− | Дано утверждение: <tex>P_1 = P_1(Q_1, \ldots, Q_n, \Psi(x_1,\dots ,x_n)) = Q_1 x_1 Q_2 x_2 \ldots Q_n x_n \Psi(x_1,\dots ,x_n)</tex> | + | Дано утверждение: <tex>P_1 = P_1(Q_1, \ldots, Q_n, \Psi(x_1,\dots ,x_n)) = Q_1 x_1 Q_2 x_2 \ldots Q_n x_n \Psi(x_1,\dots ,x_n),</tex> где <tex>\{Q_i\}_{i=1}^{n} </tex> является чередующейся последовательностью кванторов <tex>\forall</tex> и <tex>\exists</tex>. |
# Если утверждение <tex>P_1</tex> истинно, то у игрока «существует» есть набор ходов, используя который, он может победить. | # Если утверждение <tex>P_1</tex> истинно, то у игрока «существует» есть набор ходов, используя который, он может победить. | ||
# Если же утверждение <tex>P_1</tex> ложно, то у игрока «для всех» есть набор ходов, используя который, он может победить. | # Если же утверждение <tex>P_1</tex> ложно, то у игрока «для всех» есть набор ходов, используя который, он может победить. | ||
Строка 13: | Строка 25: | ||
#*: Если единственный квантор {{---}} «существует», то, по условию, есть такой параметр, что утверждение будет истинно. Его и подставит игрок «существует», после чего сразу победит. | #*: Если единственный квантор {{---}} «существует», то, по условию, есть такой параметр, что утверждение будет истинно. Его и подставит игрок «существует», после чего сразу победит. | ||
#* '''Переход:''' теорема верна, когда утверждение <tex>P_1</tex> содержит не более <tex>n-1</tex> квантора, докажем, что она верна и для утверждений, содержащих <tex>n</tex> кванторов. | #* '''Переход:''' теорема верна, когда утверждение <tex>P_1</tex> содержит не более <tex>n-1</tex> квантора, докажем, что она верна и для утверждений, содержащих <tex>n</tex> кванторов. | ||
− | #*: Пусть первый квантор «существует», тогда <tex>P_1 = \exists x_1 P_2</tex>, где <tex>P_2 = P_2(Q_2, \ldots, Q_n, \Psi(x_1,\dots ,x_n)_{x_1=const})</tex>. По условию теоремы найдётся такой параметр <tex>x_1 = x_{1_0}</tex>, что <tex>P_1</tex> истинно. Но выражение <tex>P_2</tex> истинно и содержит <tex>n-1</tex> квантор, значит, для <tex>P_2</tex> есть набор ходов игрока «существует», при котором он выигрывает. С выбранным <tex>x_1 = x_{1_0}</tex> и полученным набором ходов мы получаем выигрышную стратегию. | + | #*: Пусть первый квантор «существует», тогда <tex>P_1 = \exists x_1 P_2</tex>, где <tex>P_2 = P_2(Q_2, \ldots, Q_n, \Psi(x_1,\dots ,x_n)_{x_1=const})\,</tex>. По условию теоремы найдётся такой параметр <tex>x_1 = x_{1_0}</tex>, что <tex>P_1</tex> истинно. Но выражение <tex>P_2</tex> истинно и содержит <tex>n-1</tex> квантор, значит, для <tex>P_2</tex> есть набор ходов игрока «существует», при котором он выигрывает. С выбранным <tex>x_1 = x_{1_0}</tex> и полученным набором ходов мы получаем выигрышную стратегию. |
− | #*: Пусть теперь первый квантор «для всех», тогда <tex>P_1 = \forall x_1 \exists x_2 P_3</tex>, где <tex>P_3 = P_3(Q_3, \ldots, Q_n, \Psi(x_1, x_2, \dots ,x_n)_{x_1=const, x_2=const})</tex>. По условию теоремы для любого параметра <tex>x_1</tex> найдётся такой параметр <tex>x_2 = x_{2_0}</tex>, что <tex>P_1</tex> истинно. Но утверждение <tex>P_3</tex> истинно и содержит <tex>n-2</tex> квантора, значит, для <tex>P_3</tex> есть набор ходов игрока «существует», при котором он выигрывает. С выбранным <tex>x_2 = x_{2_0}</tex> и полученным набором ходов мы получим выигрышную стратегию. | + | #*: Пусть теперь первый квантор «для всех», тогда <tex>P_1 = \forall x_1 \exists x_2 P_3</tex>, где <tex>P_3 = P_3(Q_3, \ldots, Q_n, \Psi(x_1, x_2,\dots ,x_n)_{x_1=const, x_2=const})\,</tex>. По условию теоремы для любого параметра <tex>x_1</tex> найдётся такой параметр <tex>x_2 = x_{2_0}</tex>, что <tex>P_1</tex> истинно. Но утверждение <tex>P_3</tex> истинно и содержит <tex>n-2</tex> квантора, значит, для <tex>P_3</tex> есть набор ходов игрока «существует», при котором он выигрывает. С выбранным <tex>x_2 = x_{2_0}</tex> и полученным набором ходов мы получим выигрышную стратегию. |
# Доказательство существования выигрышной стратегии игрока «для всех» при ложном выражении <tex>\Psi</tex> аналогично. | # Доказательство существования выигрышной стратегии игрока «для всех» при ложном выражении <tex>\Psi</tex> аналогично. | ||
}} | }} | ||
Строка 23: | Строка 35: | ||
==Источники информации== | ==Источники информации== | ||
− | [https://en.wikipedia.org/wiki/True_quantified_Boolean_formula| Wikipedia {{---}} True quantified Boolean formula] | + | *[https://en.wikipedia.org/wiki/True_quantified_Boolean_formula| Wikipedia {{---}} True quantified Boolean formula] |
[[Категория:Теория формальных языков]] | [[Категория:Теория формальных языков]] | ||
[[Категория:Автоматы и регулярные языки]] | [[Категория:Автоматы и регулярные языки]] | ||
− | [[Категория: | + | [[Категория:Математическая логика]] |
Текущая версия на 19:44, 4 сентября 2022
Определение: |
В игре участвуют два игрока — «для всех» и «существует». Есть утверждение | . Игроки поочередно выбирают значения параметров. Каждый игрок выбирает значение в зависимости от предыдущих ходов. Цель игрока «существует» делать такие ходы, чтобы утверждение получилось истинным. А цель игрока «для всех» делать такие ходы, чтобы итоговое выражение получилась ложным.
Интерпретация булевых формул с кванторами как игр для двух игроков
Теорема: |
Дано утверждение: где является чередующейся последовательностью кванторов и .
|
Доказательство: |
|