Die Logik QF_UF in SMT-LIB

Bsp: die Formel (x = y)∧(f (f (g(x)))≠f (f (g(y)))) mathend000#

(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)

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

∀f, g, x, y : ((x = y)→(f (f (g(x))) = f (f (g(y))))

mathend000#