Изменения

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

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

405 байт добавлено, 18:58, 1 июня 2012
Нет описания правки
}}
Введем обозначениеобозначения: * <tex>A_i(x_{i+1}) Q_i = \sum\limits_{x_{i+2} x_i = 0}^{1}</tex> или <tex>Q_i = \ldots\sumprod\limits_{x_m x_i = 0}^{1} </tex>* <tex>s = Q_1 \ldots Q_m A(x_1, \ldots, x_m)</tex>* <tex>A_i(x_{i+1}) = Q_{i + 2} \ldots Q_m A(c_1,\ldots, c_i, x_{i+1}, ..., x_m)</tex>, где <tex>c_1, \ldots, c_i</tex> {{---}} некоторые двоичные константы.
{{Лемма
|statement=
При введенных выше обозначениях выполняются:
# Если <tex>Q_1 = \sum\limits_{x_1 = 0}^{1}</tex>, то <tex>A_0(0) + A_0(1) = ks</tex>, если <tex>Q_1 = \prod\limits_{x_1 = 0}^{1}</tex>, то <tex>A_0(0) \cdot A_0(1) = s</tex># Если <tex>Q_i = \forall sum\limits_{x_i = 0}^{1 }</tex>, то <tex> A_i(0) + A_i(1) = A_{i-1}(c_i)</tex># Если <tex>Q_i = \le i prod\le m: limits_{x_i = 0}^{1}</tex>, то <tex> A_i(0) + \cdot A_i(1) = A_{i-1}(c_i)</tex>
|proof=
proof
}}
70
правок

Навигация