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:fol_with_update_expressions [2008/04/09 00:23]
vkuncak
sav08:fol_with_update_expressions [2015/04/21 17:30] (current)
Line 21: Line 21:
 ===== Syntax Summary ===== ===== Syntax Summary =====
  
-\[\begin{array}{l}+\begin{equation*}\begin{array}{l}
   F ::= A \mid F \land F \mid F \lor F \mid \lnot F \mid \exists x.F \mid \forall x.F \\   F ::= A \mid F \land F \mid F \lor F \mid \lnot F \mid \exists x.F \mid \forall x.F \\
   A ::= R(T,​\ldots,​T) \mid T=T \mid S \subseteq S \mid S=S \\   A ::= R(T,​\ldots,​T) \mid T=T \mid S \subseteq S \mid S=S \\
Line 27: Line 27:
   U ::= f \mid U((T,​\ldots,​T):​=T) \\   U ::= f \mid U((T,​\ldots,​T):​=T) \\
   S ::= V_s \mid S \cup S \mid S \cap S \mid S \setminus S \mid \{T,​\ldots,​T\} ​   S ::= V_s \mid S \cup S \mid S \cap S \mid S \setminus S \mid \{T,​\ldots,​T\} ​
-\end{array}\]+\end{array}\end{equation*}
  
 ===== Elimination of Extensions ===== ===== Elimination of Extensions =====
Line 40: Line 40:
  
 S1 = S0 Un {a} $\leftrightarrow$ ++| ALL x. S1(x) <-> S0(x) | x=a ++ S1 = S0 Un {a} $\leftrightarrow$ ++| ALL x. S1(x) <-> S0(x) | x=a ++
 +
 +f = g ++| ALL x. f(x)=g(x) ++
  
 === Substituting Function Symbols === === Substituting Function Symbols ===
 
sav08/fol_with_update_expressions.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice