Differences

This shows you the differences between two versions of the page.

--- arithmetic_logic:start [2016/09/27 15:00] – corrected \neg A formula markus
+++ arithmetic_logic:start [2016/09/28 10:55] (current) – removed willi_bd
@@ Line 1: / Line 1: @@
-====== 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}