Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav07_lecture_23 [2007/07/02 17:23] simon.blanchoud |
sav07_lecture_23 [2007/07/02 17:51] simon.blanchoud |
||
|---|---|---|---|
| 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 | ||
| + | |||
| ==== Monadic Class of FOL ==== | ==== Monadic Class of FOL ==== | ||
| - | MFOL has : only unary predicates, no function symbol, quatifiers and logic. | + | MFOL(({{bachmairetal93setconstraintsmonadicclass.ps|Set constraints are the monadic class}})) has : only unary predicates, no function symbol, quatifiers and logic. |
| Translating this to our sets language : | Translating this to our sets language : | ||
| - | F := | + | F := S = S |
| + | | S ⊆ S | ||
| + | | card(S) ≥ k | ||
| + | | card(S) = k | ||
| + | | F ∧ F | ||
| + | | ¬ F | ||
| + | | ∃v.F | ||
| + | S := v | ||
| + | | S ∪ S | ||
| + | | S ∩ S | ||
| + | | S' | ||
| + | | ∅ | ||
| + | | 1 | ||
| + | |||
| + | Where : | ||
| + | * $card(S) \geq k$ is syntactic sugar to represent a unary operator, as $k$ is not a variable, that compare the cardinality of $S$ with $k$ | ||
| + | * $k \geq 0$ is an integer | ||
| + | * $S'$ is the complement set of $S$ | ||
| + | * $1$ represents the whole universe | ||
| + | |||
| + | In order to agree with our definitions of set constraints, we need to eliminate : | ||
| + | * $S_1 = S_2 \rightarrow S_1 \subseteq S_2 \wedge S_2 \subseteq S_1 $ | ||
| + | * $S_1 \subseteq S_2 \rightarrow card(S_1 \cup S_2') = 0$ | ||
| + | |||
| + | We then have to be able to represent the following formulas : | ||
| + | * $\neg(card(s) \geq k) \rightarrow \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\] | ||
| + | |||
| + | After elimination of the quantifiers, deciding the result of the formula is trivial. | ||
| - | Deciding monadic class (({{bachmairetal93setconstraintsmonadicclass.ps|Set constraints are the monadic class}})) | + | 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 ! |
| - | * reduction to boolean algebras (MSOL fragment, has QE) | + | |
| - | * small model property | + | |
| - | * resolution variants | + | |