LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
using_automata_to_decide_presburger_arithmetic [2009/04/29 10:53]
vkuncak
using_automata_to_decide_presburger_arithmetic [2009/04/29 10:55]
vkuncak
Line 83: Line 83:
 Therefore, to check if $F$ is satisfiable,​ we construct $A(F)$ automaton and check whether the graph of $A(F)$ has a reachable accepting state. Therefore, to check if $F$ is satisfiable,​ we construct $A(F)$ automaton and check whether the graph of $A(F)$ has a reachable accepting state.
  
 +**Example:​** Step-by-step construction of automaton for 
 +\[
 +   \lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z)
 +\]