Ackermann-Transformation

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

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

  für alle F_i = g(F_i1,…, F_ik), F_j = g(F_j1,…, F_jk) mathend000# mit i≠j mathend000#:

  (f_i1 = f_j1∧…∧f_ik = f_jk)→f_i = f_j mathend000#

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