Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
using_automata_to_decide_presburger_arithmetic [2009/04/29 10:53]
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 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 
 +\begin{equation*}
 +   \lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z)
 +\end{equation*}
  
 
using_automata_to_decide_presburger_arithmetic.txt · Last modified: 2015/04/21 17:26 (external edit)
 
© EPFL 2018 - Legal notice