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

Материал из Викиконспекты
Перейти к: навигация, поиск

Введём понятие арифметизации булевых формул. Пусть нам дана формула [math]\phi(x_1 \ldots x_m)[/math]. Сделаем следующие преобразования и получим формулу [math]A_\phi(x_1, x_2, \ldots, x_m)[/math]:

  1. [math]x_i \to x_i[/math];
  2. [math]\lnot x \to 1 - x[/math];
  3. [math]\varphi \land \psi \to A_\varphi \cdot A_\psi[/math];
  4. [math]\varphi \lor \psi \to 1 - (1 - A_\varphi) \cdot (1 - A_\psi)[/math];
  5. [math]\exists x \varphi(x) \to \sum\limits_{x=0}^{1} A_\varphi(x)[/math];
  6. [math]\forall x \varphi(x) \to \prod\limits_{x=0}^{1} A_\varphi(x)[/math].

Заметим, что если [math]\phi[/math] не содержит кванторов, то [math]|A_\phi| \le C |\phi|[/math] , где [math]C[/math] — некоторая константа.

Лемма (1):
[math]\phi(x_1 \ldots x_m) = A_\phi(x_1, \ldots, x_m)[/math].
Доказательство:
[math]\triangleright[/math]
proof
[math]\triangleleft[/math]

Введем обозначения:

  • [math]Q_i = \sum\limits_{x_i = 0}^{1}[/math] или [math]Q_i = \prod\limits_{x_i = 0}^{1}[/math]
  • [math]s = Q_1 \ldots Q_m A(x_1, \ldots, x_m)[/math]
  • [math]A_i(x_{i+1}) = Q_{i + 2} \ldots Q_m A(c_1,\ldots, c_i, x_{i+1}, ..., x_m)[/math], где [math]c_1, \ldots, c_i[/math] — двоичные константы.
Лемма (2):
При введенных выше обозначениях выполняются:
  1. Если [math]Q_1 = \sum\limits_{x_1 = 0}^{1}[/math], то [math]A_0(0) + A_0(1) = s[/math], если [math]Q_1 = \prod\limits_{x_1 = 0}^{1}[/math], то [math]A_0(0) \cdot A_0(1) = s[/math]
  2. Если [math]Q_i = \sum\limits_{x_i = 0}^{1}[/math], то [math] A_i(0) + A_i(1) = A_{i-1}(c_i)[/math]
  3. Если [math]Q_i = \prod\limits_{x_i = 0}^{1}[/math], то [math] A_i(0) \cdot A_i(1) = A_{i-1}(c_i)[/math]
Доказательство:
[math]\triangleright[/math]
proof
[math]\triangleleft[/math]