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
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)
 
© EPFL 2018 - Legal notice