Entscheidbare Fälle

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

in SMT-LIB: nur außen existentiell.

$\displaystyle \exists$f, g, x, y : ¬((x = y) $\displaystyle \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:

$\displaystyle \forall$f, g, x, y : ((x = y) $\displaystyle \rightarrow$ (f (f (g(x))) = f (f (g(y))))



2009-06-22