Differences

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

--- sav08:qe_for_presburger_arithmetic [2009/04/23 09:27]
vkuncak
+++ sav08:qe_for_presburger_arithmetic [2009/04/23 09:44]
vkuncak
@@ Line 39: / Line 39: @@
 **Coefficient next to** $y$:
-To eliminate $\exists y$ from such conjunction, we wish to ensure that the coefficient next to $y$ is one or minus one. Note that $0 < t$ is equivalent to $0 < c\, t$ and $K \mid t$ is equivalent to $c\, K \mid c\, t$ for $c$ a positive integer.  If $K_1,\ldots,K_n$ are all coefficients next to $y$ in the formula, let $M$ be a positive integer such that $K_i \mid M$ for all $i$, $1 \le i \le n$ (for example, let $M$ be the least common multiple of $K_1,\ldots,K_n$).  Multiply each literal where $y$ occurs in subterm $K_i y$ by constant $M/|K_i|$.
+To eliminate $\exists y$ from such conjunction, we wish to ensure that the coefficient next to $y$ is one or minus one.
+//Observation:// $0 < t$ is equivalent to $0 < c\, t$ and $K \mid t$ is equivalent to $c\, K \mid c\, t$ for $c$ a positive integer.
+If $K_1,\ldots,K_n$ are all coefficients next to $y$ in the formula, let $M$ be a positive integer such that $K_i \mid M$ for all $i$, $1 \le i \le n$ (for example, let $M$ be the least common multiple of $K_1,\ldots,K_n$).  Multiply each literal where $y$ occurs in subterm $K_i y$ by constant $M/|K_i|$.
 What is the coefficient next to $y$ in the resulting formula?  ++| either $M$ or $-M$ ++