====== Arithmetization ======

Arithmetization can be viewed in many contexts. This topic is referring to the arithmetization of mathematical theorems into integer optimization problems and therefore open the possibility to computer-based mathematical proving.

===== Introduction =====

Any boolean formula can be transformed into a 3 way conjunctive normal form. Any 3 way conjunctive normal form boolean formula itself can be transformed into an integer nonlinear equation. With the transformations

\begin{align}
\left( A \vee B \right) & \mapsto & 1 - \left( 1-A \right) \cdot \left( 1-B \right) \\
\left( A \wedge B \right) & \mapsto & A \cdot B \\
\neg A & \mapsto & 1-A 
\end{align}

Notice that De Morgan's rules apply since
\begin{equation}
\neg \left( A \wedge B \right) \Leftrightarrow \left( \neg A \vee \neg B \right) \mapsto 1 - A \cdot B
\end{equation}