• English only

# Differences

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

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 ===