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
Substituting Function Symbols
1)
a,b):=c)(x,y) =
=== Sets ===
Set variables (not quantified).
Set operations
,
,
,
.
===== Syntax Summary =====
\[\begin{array}{l}
F(ite(p,x,y
![Math $\cup$](/w/lib/exe/fetch.php?media=wiki:latex:/img655ba4ff82d4b3329109a26a2295efe1.png)
![Math $\cap$](/w/lib/exe/fetch.php?media=wiki:latex:/img7ab28e3f02aa13bfc8dd97fe3b995ecb.png)
![Math $\setminus$](/w/lib/exe/fetch.php?media=wiki:latex:/img1df00dc7bb553d90756ea6002bd9fbb3.png)
![Math $\{x,y\}$](/w/lib/exe/fetch.php?media=wiki:latex:/img5325efe93ef831d6cf4368b6a8386f1d.png)
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)
![Math $\leftrightarrow$](/w/lib/exe/fetch.php?media=wiki:latex:/img43c24ae4490ffb3a4e8e30d0250ffd2c.png)