Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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] (current)
Line 3: Line 3:
 Consider a simple language of sets: Consider a simple language of sets:
  
-\[+\begin{equation*}
 \begin{array}{l} \begin{array}{l}
    S ::= V \mid S \cup S \mid S \cap S \mid S \setminus S \mid \mathbf{U} \mid \emptyset \\    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 \\    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 ...    c ::= 0 \mid 1 \mid 2 \mid ...
 \end{array} \end{array}
-\]+\end{equation*}
  
 We show that this language is decidable by reduction to universal class. We show that this language is decidable by reduction to universal class.
 
sav08/deciding_a_language_of_sets_and_relations.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice