Differences
This shows you the differences between two versions of the page.
|
sav08:deciding_a_language_of_sets_and_relations [2009/05/14 12:05] vkuncak |
sav08:deciding_a_language_of_sets_and_relations [2015/04/21 17:30] |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Deciding a Language of Sets (and Relations) ====== | ||
| - | |||
| - | 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 by reduction to universal class. | ||
| - | |||
| - | 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. | ||