This is an old revision of the document!

FOL with Update Expressions

Syntactic extension of FOL with if-then-else, function update, sets.

If-Then-Else

ite(p,x,y) = if p then x else y

Function Update

f (a:=b)(x) = ite(x=a,b,f(x))

f ¹⁾ $\leftrightarrow$ F(z) & z=ite(p,x,y)

S1 = S0 Un {a} $\leftrightarrow$ ALL x. S1(x) ↔ S0(x) | x=a

Substituting Function Symbols

¹⁾

a,b):=c)(x,y) = === Sets === Set variables (not quantified). Set operations $\cup$ , $\cap$ , $\setminus$ , $\{x,y\}$ . ===== Syntax Summary ===== \[\begin{array}{l}

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 \\
T ::= V_o \mid U(T,\ldots,T) \mid ite(F,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\}

\end{array}\] ===== Elimination of Extensions ===== f(a:=b)(x) = f((a,b):=c)(x,y) = z=ite(p,x,y) $\leftrightarrow$ F(ite(p,x,y