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
Next revision Both sides next revision
sav07_lecture_3 [2007/03/22 10:59]
yuanjianwz 		sav07_lecture_3 [2007/03/22 16:20]
yuanjianwz
Line 96: Line 96:
  
 We can apply these rules to reduce the size of formulas. We can apply these rules to reduce the size of formulas.
 +
  
  
 ==== Approximation ==== ==== Approximation ====
  
-If (F -> G) is value, we say that F is stronger than F and we say G is weaker than F.+If (F -> G) is valid, we say that F is stronger than F and we say G is weaker than F.
  
 When a formula would be too complicated,​ we can instead create a simpler approximate formula. ​ To be sound, if our goal is to prove a property, we need to generate a *larger* relation, which corresponds to a weaker formula describing a relation, and a stronger verification condition. ​ (If we were trying to identify counterexamples,​ we would do the opposite). When a formula would be too complicated,​ we can instead create a simpler approximate formula. ​ To be sound, if our goal is to prove a property, we need to generate a *larger* relation, which corresponds to a weaker formula describing a relation, and a stronger verification condition. ​ (If we were trying to identify counterexamples,​ we would do the opposite).
Line 214: Line 215:
  
 Proof: small model theorem. Proof: small model theorem.
 +
 +
 +
 +
 +
 +
 +
  
 ==== Small model theorem for Quantifier-Free Presburger Arithmetic (QFPA) ==== ==== Small model theorem for Quantifier-Free Presburger Arithmetic (QFPA) ====
 +
 +The idea is to reduce the case, for example:
 +//​∃x,​y,​z.F//​
 +reduce to 
 +//∃x≤ M,y≤ M,z ≤ M.F// 
 +Then we try to figure out the boundary M.
 +
 +Another example:
 +//¬t1 < t2// 
 +reduce to 
 +//​t2+1≤t1// ​
 +
 +How about the not equal ?
 +
 +//t1≠t2//
 +can be reduced to  ​
 +//(t1 < t2 ) ∨ (t2 < t1) => (t1 ≤ t2-1) ∨ (t2 ≤ t1-1)//
  
 First step: transform to disjunctive normal form. First step: transform to disjunctive normal form.