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
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] (current)
Line 13: Line 13:
 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. 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{equation*}
 \begin{array}{rcl} \begin{array}{rcl}
       F & ::= & A \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid \lnot F \mid        F & ::= & A \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid \lnot F \mid 
Line 25: Line 25:
       K & ::= & \ldots {-2} \mid -1 \mid 0 \mid 1 \mid 2 \ldots       K & ::= & \ldots {-2} \mid -1 \mid 0 \mid 1 \mid 2 \ldots
     \end{array}     \end{array}
-\]+\end{equation*}
  
 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}|$. 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}|$.
 +
  
  
Line 43: Line 44:
  
 Eliminate the quantifier $X$ from the following formula: Eliminate the quantifier $X$ from the following formula:
-\[+\begin{equation*}
 \exists X. A \subseteq X \land X \cup B = B \land |X \cap A| = 2 |A| + 1 \exists X. A \subseteq X \land X \cup B = B \land |X \cap A| = 2 |A| + 1
-\]+\end{equation*}
  
 ++++ | ++++ |
-\[+\begin{equation*}
 A \subseteq X \Rightarrow |A \cap X^c| = 0 A \subseteq X \Rightarrow |A \cap X^c| = 0
-\] +\end{equation*} 
-\[+\begin{equation*}
 X \cup B = B \Rightarrow |(X \cup B) \cap B^c| = 0 \land |B \cap (X \cup B)^c| = 0 X \cup B = B \Rightarrow |(X \cup B) \cap B^c| = 0 \land |B \cap (X \cup B)^c| = 0
-\] +\end{equation*} 
-The resulting formula ​is then: \\+The starting point after transformation to cardinality constraints ​is: \\
 <​latex>​ <​latex>​
 k_1 = |A| \land \\ k_1 = |A| \land \\
Line 66: Line 67:
 k_5 = 0 k_5 = 0
 </​latex>​ </​latex>​
- 
  
 ++++ ++++
Line 81: Line 81:
  
 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: 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:
-\[+\begin{equation*}
     \bigcup_{i=1}^m x_i^{\alpha_i}     \bigcup_{i=1}^m x_i^{\alpha_i}
-\]+\end{equation*}
 where $x^\alpha$ is either $x$ or $x^c$ (complement of $x$). where $x^\alpha$ is either $x$ or $x^c$ (complement of $x$).
  
Line 89: Line 89:
  
 Then use Then use
-\[+\begin{equation*}
    |b| = |s_{i_1}| + \ldots + |s_{i_k}|    |b| = |s_{i_1}| + \ldots + |s_{i_k}|
-\]+\end{equation*}
 We therefore assume that the only occurence of sets and set operators is within $|s|$ where $s$ is a Venn region. We therefore assume that the only occurence of sets and set operators is within $|s|$ where $s$ is a Venn region.
  
Line 98: Line 98:
  
 Transform formula to prenex form Transform formula to prenex form
-\[+\begin{equation*}
    Q_p v_p. \dots Q_1 v_1. G_1(|s_1|,​\ldots,​|s_n|)    Q_p v_p. \dots Q_1 v_1. G_1(|s_1|,​\ldots,​|s_n|)
-\]+\end{equation*}
 where $F$ is quantifier-free. 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 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
-\[+\begin{equation*}
       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)       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)
-\]+\end{equation*}
 Note that $G_1(l_1,​\ldots,​l_q)$ is a quantifier-free PA formula.  ​ Note that $G_1(l_1,​\ldots,​l_q)$ is a quantifier-free PA formula.  ​
  
Line 112: Line 112:
  
 We will eliminate integer and set quantifiers from the entire subformula $Q_p v_p. \dots Q_1 v_1$ We will eliminate integer and set quantifiers from the entire subformula $Q_p v_p. \dots Q_1 v_1$
-\[+\begin{equation*}
 \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) \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)
-\]+\end{equation*}
 Indeed, we can always transform this formula to a quantifier-free formula by substituting $|s_i|$ back into $G_1$. Indeed, we can always transform this formula to a quantifier-free formula by substituting $|s_i|$ back into $G_1$.
  
 
sav08/deciding_boolean_algebra_with_presburger_arithmetic.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice