Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

sav07_lecture_23 [2007/07/02 17:51]
simon.blanchoud
sav07_lecture_23 [2015/04/21 17:32] (current)
Line 67: Line 67:
  
 We can then introduce $S_p$ as the set variable of the called methods : We can then introduce $S_p$ as the set variable of the called methods :
- \[\forall p \in P . S_p \subseteq \left \lbrace m | \left ( info(p), m \right ) \in r^*, r = \lbrace (x,y) | x = over(y) \rbrace \right \rbrace \]+ \begin{equation*}\forall p \in P . S_p \subseteq \left \lbrace m | \left ( info(p), m \right ) \in r^*, r = \lbrace (x,y) | x = over(y) \rbrace \right \rbrace \end{equation*}
  
 We also define $S_I$ as the set of all possibly called methods that we can build using the following formula : We also define $S_I$ as the set of all possibly called methods that we can build using the following formula :
-\main  \in S_I \bigwedge_{m \in M} \left ( m \in S_I \wedge p \in calls(m) \right ) \Rightarrow S_p \subseteq S_I \bigwedge_{m \in M} m \in S_I \Rightarrow inst(m) \subseteq S_I \]+\begin{equation*} ​main  \in S_I \bigwedge_{m \in M} \left ( m \in S_I \wedge p \in calls(m) \right ) \Rightarrow S_p \subseteq S_I \bigwedge_{m \in M} m \in S_I \Rightarrow inst(m) \subseteq S_I \end{equation*}
  
  
Line 130: Line 130:
   * First-order theory : $\forall x \exist y . f(f(a,a), x) = f(y, a) \wedge y \neq a$   * First-order theory : $\forall x \exist y . f(f(a,a), x) = f(y, a) \wedge y \neq a$
 This is First-Order Logic (FOL) with variables ! We can relate this to set constraints This is First-Order Logic (FOL) with variables ! We can relate this to set constraints
 +
  
  
Line 165: Line 166:
   * $\neg(card(s) = k) \rightarrow card(S) \geq k+1 \vee \bigvee_{i=0}^{k-1} card(S) = i$   * $\neg(card(s) = k) \rightarrow card(S) \geq k+1 \vee \bigvee_{i=0}^{k-1} card(S) = i$
  
-We can then perform quantifier elimination. Note that this is not possible in case we do not have the $card$ operator : \[\exists v.card(S_1 \cap v) = k_1 \wedge card(S_1 \cap v') = k_2 \Rightarrow card(S_1) = k_1 + k_2\]+We can then perform quantifier elimination. Note that this is not possible in case we do not have the $card$ operator : \begin{equation*}\exists v.card(S_1 \cap v) = k_1 \wedge card(S_1 \cap v') = k_2 \Rightarrow card(S_1) = k_1 + k_2\]
  
 After elimination of the quantifiers,​ deciding the result of the formula is trivial. After elimination of the quantifiers,​ deciding the result of the formula is trivial.
- 
-If we add to our language the possibility ot replace $k$ by $card(S)$ then this new language is still decidable and is equivalent to Presbulgarian arithmetic ! 
  
  
  
  
 
sav07_lecture_23.txt · Last modified: 2015/04/21 17:32 (external edit)