Булевые формулы с кванторами как игры для двух игроков — различия между версиями
Ponomarev (обсуждение | вклад) |
Ponomarev (обсуждение | вклад) (→Источники информации) |
||
(не показаны 4 промежуточные версии 2 участников) | |||
Строка 16: | Строка 16: | ||
{{Теорема | {{Теорема | ||
|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>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> ложно, то у игрока «для всех» есть набор ходов, используя который, он может победить. | ||
Строка 35: | Строка 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] |
[[Категория:Теория формальных языков]] | [[Категория:Теория формальных языков]] | ||
[[Категория:Автоматы и регулярные языки]] | [[Категория:Автоматы и регулярные языки]] | ||
− | [[Категория: | + | [[Категория:Математическая логика]] |
Версия 23:18, 14 марта 2018
Определение: |
В игре участвуют два игрока — «для всех» и «существует». Есть утверждение | . Игроки поочередно выбирают значения параметров. Каждый игрок выбирает значение в зависимости от предыдущих ходов. Цель игрока «существует» делать такие ходы, чтобы утверждение получилось истинным. А цель игрока «для всех» делать такие ходы, чтобы итоговое выражение получилась ложным.
Интерпретация булевых формул с кванторами как игр для двух игроков
Теорема: |
Дано утверждение: где является чередующейся последовательностью кванторов и .
|
Доказательство: |
|