Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
using_automata_to_decide_presburger_arithmetic [2009/04/29 10:55] vkuncak |
using_automata_to_decide_presburger_arithmetic [2015/04/21 17:26] (current) |
||
---|---|---|---|
Line 28: | Line 28: | ||
v: 1 0 0 0 0 | v: 1 0 0 0 0 | ||
This string represents the satisfying assignment $\{(x,4),\ (y,3),\ (z,4),\ (v,1)\}$ for the above formula. If we take the valid formula | This string represents the satisfying assignment $\{(x,4),\ (y,3),\ (z,4),\ (v,1)\}$ for the above formula. If we take the valid formula | ||
- | \[ | + | \begin{equation*} |
\lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z) | \lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z) | ||
- | \] | + | \end{equation*} |
the corresponding automaton accepts all strings. **(End of example.)** | the corresponding automaton accepts all strings. **(End of example.)** | ||
Line 84: | Line 84: | ||
**Example:** Step-by-step construction of automaton for | **Example:** Step-by-step construction of automaton for | ||
- | \[ | + | \begin{equation*} |
\lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z) | \lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z) | ||
- | \] | + | \end{equation*} |