Ackermann-Transformation

...von Formel F in QF_UF nach Formel F' in equalitiy logic (= QF_UF mit nur nullstelligen Symbolen)

• ersetze jeden vorkommenden Teilterm F_i durch ein neues nullstelliges Symbol f_i
• füge functional consistency constraints hinzu:

  für alle F_i = g(F_i1,..., F_ik), F_j = g(F_j1,..., F_jk) mit i $\neq$ j:

  (f_i1 = f_j1 $\wedge$...$\wedge$ f_ik = f_jk) $\rightarrow$ f_i = f_j

Satz: F erfüllbar $\iff$ F' erfüllbar.