Differences
This shows you the differences between two versions of the page.
Next revision Both sides next revision | |||
sav08:deciding_a_language_of_sets_and_relations [2008/04/03 13:45] vkuncak created |
sav08:deciding_a_language_of_sets_and_relations [2008/04/03 13:49] vkuncak |
||
---|---|---|---|
Line 3: | Line 3: | ||
Consider a simple language of sets: | Consider a simple language of sets: | ||
+ | \[ | ||
+ | \begin{array}{l} | ||
+ | S ::= V \mid S \cup S \mid S \cap S \mid S \setminus S \mid \mathbf{U} \mid \emptyset \\ | ||
+ | A ::= (S = S) \mid (S \subseteq S) \mid card(S){=}c \mid card(S) \leq c \mid card(S) \geq c \\ | ||
+ | F ::= F \lor F \mid F \land F \mid \lnot F \\ | ||
+ | c ::= 0 \mid 1 \mid 2 \mid ... | ||
+ | \end{array} | ||
+ | \] | ||
+ | |||
+ | We show that this language is decidable. | ||
+ | |||
+ | ===== References ===== | ||
* [[http://lara.epfl.ch/~kuncak/papers/KuncakRinard05DecisionProceduresSetValuedFields.html|Decision Procedures for Set-Valued Fields]] | * [[http://lara.epfl.ch/~kuncak/papers/KuncakRinard05DecisionProceduresSetValuedFields.html|Decision Procedures for Set-Valued Fields]] | ||