Differences

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

--- sav08:deciding_a_language_of_sets_and_relations [2008/04/03 13:49]
vkuncak
+++ sav08:deciding_a_language_of_sets_and_relations [2015/04/21 17:30] (current)
@@ Line 3: / Line 3: @@
 Consider a simple language of sets:
-\[
+\begin{equation*}
 \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 \\
+   F ::= F \lor F \mid F \land F \mid \lnot F \mid A \\
    c ::= 0 \mid 1 \mid 2 \mid ...
 \end{array}
-\]
+\end{equation*}
-We show that this language is decidable.
+We show that this language is decidable by reduction to universal class.
-===== References =====
+While BAPA is more expressive with respect to cardinalities, the advantage of the present method is that it allows the use of certain relations.
   * [[http://lara.epfl.ch/~kuncak/papers/KuncakRinard05DecisionProceduresSetValuedFields.html|Decision Procedures for Set-Valued Fields]]
+However, see [[http://lara.epfl.ch/~kuncak/papers/WiesETAL09CombiningTheorieswithSharedSetOperations.html|On Combining Theories with Shared Set Operations]] for a way to combine BAPA with logics that support relations.