Изменения

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

Арифметизация булевых формул с кванторами

618 байт добавлено, 23:36, 2 июня 2012
Нет описания правки
|about=2
|statement=
Пусть <tex>Q_1 \ldots Q_m \phi(x_1, \ldots, x_m)</tex> {{---}} булева формула с кванторами, переходящая в процессе арифметизации в <tex>s = R_1 \ldots R_m A_\phi(x_1, \ldots, x_m)</tex>.  <tex>c_1, \ldots, c_m</tex> {{---}} двоичные константы.  Обозначим через <tex>A_i(x_{i+1}) = R_{i+2} \ldots R_m A_\phi(c_1, \ldots, c_i, x_{i+1}, \ldots, x_m)</tex>, где <tex>0 \le i \le m - 1</tex>. Тогда:### Если <tex>R_1 = \sum</tex>, то <tex>A_0(0) + A_0(1) = s</tex>, если ;##Если <tex>R_1 = \prod</tex>, то <tex>A_0(0) \cdot A_0(1) = s</tex>.# <tex>\forall i : 1 \le i \le m - 1</tex> если ##Если <tex>R_{i+1} = \sum</tex>, то <tex> A_i(0) + A_i(1) = A_{i-1}(c_i)</tex>, если ;##Если <tex>R_{i+1} = \prod</tex>, то <tex>A_i(0) \cdot A_i(1) = A_{i-1}(c_i)</tex>.
|proof=
proofДокажем пункты 1.1 и 2.1. Для остальных пунктов доказательство аналогично. 1.1. <tex>s=\sum\limits_{x_1 = 0}^{1}R_2\ldots R_m(x_1, x_2, \ldots, x_m)=R_2 \ldots R_m</tex><tex>(0, x_2, \ldots, x_m) + R_2 \ldots R_m(1, x_2, \ldots, x_m)=A_0(0) + A_0(1)</tex> 2.1. <tex>A_{i-1}(c_i)=\sum\limits_{x_{i+1} = 0}^{1}R_{i+2}\ldots R_m</tex><tex>(c_1, \ldots, c_{i-1}, c_i, x_{i+1}, \ldots x_m)=R_{i+2} \ldots R_m</tex><tex>(c_1, \ldots, c_i, 0, x_{i+2}, \ldots, x_m) + R_{i+2} \ldots R_m</tex><tex>(c_1, \ldots, c_i, 1, x_{i+2}, \ldots, x_m)=A_i(0) + A_i(1)</tex>
}}
70
правок

Навигация