Entscheidbare Fälle

...durch Einschränkung der Position der Quantoren.

in SMT-LIB: nur außen existentiell.

$$\exists$$f, g, x, y : ¬((x = y) $$\rightarrow$$ (f (f (g(x))) = f (f (g(y))))

(benchmark check  :logic QF_UF
:extrafuns ((f U U)(g U U)(x U)(y U))
:formula (not (implies (= x y) 
                  (= (f(f(g x))) (f(f(g y)))) ))  )

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