LARA

Differences

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

Link to this comparison view

sav08:deciding_boolean_algebra_with_presburger_arithmetic [2010/05/10 18:16]
evka
sav08:deciding_boolean_algebra_with_presburger_arithmetic [2015/04/21 17:30]
Line 1: Line 1:
-====== Deciding Boolean Algebra with Presburger Arithmetic ====== 
- 
-===== Motivation ===== 
- 
-{{sav08:​bapa-example.png|BAPA Program Example}} 
- 
-{{sav08:​bapa-htriple.png|BAPA Hoare Triple}} 
- 
-{{sav08:​bapa-vc.png|BAPA Verification Condition}} 
- 
-===== Definition of BAPA ===== 
- 
-See [[http://​lara.epfl.ch/​~kuncak/​papers/​KuncakETAL06DecidingBooleanAlgebraPresburgerArithmetic.pdf|Figure 3 on page 5 of the paper]] and compare to its special cases: BA and PA. 
- 
-\[ 
-\begin{array}{rcl} 
-      F & ::= & A \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid \lnot F \mid  
-                \exists x.F \mid \forall x.F \mid 
-                \exists k.F \mid \forall k.F \\ 
-      A & ::= & B_1 = B_2 \mid B_1 \subseteq B_2 \mid  
-               T_1 = T_2 \mid T_1 < T_2 \mid (K{|}T) \\ 
-      B & ::= & x \mid \mathbf{0} \mid \mathbf{1} 
-                \mid B_1 \cup B_2 \mid B_1 \cap B_2 \mid B^{c} \\ 
-      T & ::= & k \mid K \mid maxc \mid T_1 + T_2 \mid K \cdot T \mid \ \q{|} B \q{|} \\ 
-      K & ::= & \ldots {-2} \mid -1 \mid 0 \mid 1 \mid 2 \ldots 
-    \end{array} 
-\] 
- 
-Semantics: we consider the theory of models where integers are interpreted as integers and sets are interpreted as subsets of some finite set.  For each finite set we have one interpretation. ​ (If we prove a valid formula, it will hold for arbitrarily large finite universes.) ​ $\mathbf{0},​\mathbf{1}$ are empty and universal set.  We interpret constant $maxc$ as $|\mathbf{1}|$. 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
- 
-===== Example ===== 
- 
-Eliminate the quantifier $X$ from the following formula: 
-\[ 
-\exists X. A \subseteq X \land X \cup B = B \land |X \cap A| = 2 |A| + 1 
-\] 
- 
-++++ | 
-\[ 
-A \subseteq X \Rightarrow |A \cap X^c| = 0 
-\] 
-\[ 
-X \cup B = B \Rightarrow |(X \cup B) \cap B^c| = 0 \land |B \cap (X \cup B)^c| = 0 
-\] 
-The resulting formula is then: \\ 
-<​latex>​ 
-k_1 = |A| \land \\ 
-k_2 = |X \cap A| \land \\ 
-k_3 = |A \cap X^c| \land \\ 
-k_4 = |(X \cup B) \cap B^c| \land \\ 
-k_5 = |B \cap (X \cup B)^c| \land \\ 
-k_2 = 2 k_1 + 1 \land  
-k_3 = 0 \land  
-k_4 = 0 \land  
-k_5 = 0 
-</​latex>​ 
- 
- 
-++++ 
- 
-===== Simplifying Atomic Formulas ===== 
- 
-For sets $x,y$: 
- 
-$x = y$ becomes $x \subseteq y\ \land\ y \subseteq x$ 
- 
-$x \subseteq y$ becomes $|x \cap y^c|=0$ 
- 
-Result: all set variables and operators occur within $|b|$ formula where $b$ is expression built from set variables, $\mathbf{0},​\mathbf{1},​\cap,​\cup,​\_^c$. 
- 
-Transform $b$ into union of disjoint Venn regions. ​ Let $s_1,​\ldots,​s_m$ be all set variables. ​ Venn regions are connected regions in the Venn diagram, and are analogous to conjunctive normal form: 
-\[ 
-    \bigcup_{i=1}^m x_i^{\alpha_i} 
-\] 
-where $x^\alpha$ is either $x$ or $x^c$ (complement of $x$). 
- 
-Now observe that each set expression $b$ is a disjoint union of certain Venn regions. ​ It is union of precisely those regions that belong to disjunctive normal form of the corresponding propositional formula. 
- 
-Then use 
-\[ 
-   |b| = |s_{i_1}| + \ldots + |s_{i_k}| 
-\] 
-We therefore assume that the only occurence of sets and set operators is within $|s|$ where $s$ is a Venn region. 
- 
- 
-===== Separating BA and PA Part ===== 
- 
-Transform formula to prenex form 
-\[ 
-   Q_p v_p. \dots Q_1 v_1. G_1(|s_1|,​\ldots,​|s_n|) 
-\] 
-where $F$ is quantifier-free. 
- 
-For each expression $|s_i|$ in $G_1(|s_1|,​\ldots,​|s_n|)$ introduce a fresh variable $l_i$ that denotes the value $|s_i|$. ​ We obtain 
-\[ 
-      Q_p v_p. \dots Q_1 v_1. \exists^+ l_1.\ldots \exists l_q. \left(\bigwedge_{i=1}^q |s_i|=l_i \right)\ \land\ G_1(l_1,​\ldots,​l_q) 
-\] 
-Note that $G_1(l_1,​\ldots,​l_q)$ is a quantifier-free PA formula.  ​ 
- 
-Here $\exists^+ l.F$ denotes $\exists l. 0 \le l \land F$. 
- 
-We will eliminate integer and set quantifiers from the entire subformula $Q_p v_p. \dots Q_1 v_1$ 
-\[ 
-\exists^+ l_1.\ldots \exists l_q. \left(\bigwedge_{i=1}^q |s_i|=l_i \right)\ \land\ G_1(l_1,​\ldots,​l_q) 
-\] 
-Indeed, we can always transform this formula to a quantifier-free formula by substituting $|s_i|$ back into $G_1$. 
- 
-In which parts of this formula do we find variables $v_p,​\ldots,​v_1$ that we wish to eliminate 
-  * integer variables? ++ | in $G_1(l_1,​\ldots,​l_q)$ ++ 
-  * set variables? ++ | in $\displaystyle\bigwedge_{i=1}^q |s_i|=l_i$ ++ 
- 
-===== Eliminating Quantifiers ===== 
- 
-==== Eliminating Integer Existential ==== 
- 
- 
-==== Eliminating Set Existential ==== 
- 
-**Lemma:** 
-Let $B_1, B_2$ be two finite disjoint sets and $L_1,​L_2,​K_1,​K_2$ non-negative integers. ​ Then the following two conditions are equivalent: 
-  * there exists a finite set $A$ such that: $|B_1 \cap A|=L_1$, $|B_1 \setminus A|=K_1$, $|B_2 \cap A|=L_2$, and $|B_2 \setminus A|=K_2$; 
-  * $|B_1|=L_1+K_1$ and $|B_2|=L_2+K_2$. 
- 
-==== Eliminating Universals ==== 
- 
-Express them using negation and existentials.