Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:deciding_boolean_algebra_with_presburger_arithmetic [2010/05/10 18:15] evka |
sav08:deciding_boolean_algebra_with_presburger_arithmetic [2010/05/10 18:16] evka |
||
|---|---|---|---|
| Line 28: | Line 28: | ||
| 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 50: | Line 53: | ||
| 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 | ||
| \] | \] | ||
| + | The resulting formula is then: \\ | ||
| <latex> | <latex> | ||
| k_1 = |A| \land \\ | k_1 = |A| \land \\ | ||
| - | k_2 = |X \cap A| \land | + | k_2 = |X \cap A| \land \\ |
| - | k_3 = |A \cap X^c| \land | + | k_3 = |A \cap X^c| \land \\ |
| - | k_4 = |(X \cup B) \cap B^c| \land | + | k_4 = |(X \cup B) \cap B^c| \land \\ |
| - | k_5 = |B \cap (X \cup B)^c| \land | + | k_5 = |B \cap (X \cup B)^c| \land \\ |
| k_2 = 2 k_1 + 1 \land | k_2 = 2 k_1 + 1 \land | ||
| k_3 = 0 \land | k_3 = 0 \land | ||