\begin{slide}{Die Logik QF\_UF in SMT-LIB}

Bsp: die Formel \( (x=y) \wedge  (f(f(g(x))) \neq f(f(g(y)))) \)

\begin{verbatim}
(set-logic QF_UF) (declare-sort U 0)
(declare-fun f (U) U) (declare-fun g (U) U)
(declare-fun x () U) (declare-fun y () U)
(assert (and (= x y) 
          (not (= (f (f (g x))) (f (f (g y)))))))
(check-sat)
\end{verbatim}

ist nicht erfüllbar, d. h. das Gegenteil ist allgemeingültig:

\[ \forall f,g,x,y: ((x=y)\rightarrow (f(f(g(x))) = f(f(g(y)))) \]

\end{slide}

