Vereinfachung von Array-Formeln:

• store mathend000# entfernen:

  ersetze store(a, i, e) mathend000# durch a' mathend000# und füge Constraints hinzu:

  select(a', i) = e∧(∀j : j≠i→select(a', j) = select(a', j)) mathend000#.

• ersetze ¬∀j : P(j) mathend000# durch ¬P(z) mathend000# mit neuer Variablen z mathend000#

• ersetze ∀j : P(j) mathend000# durch $\bigwedge_{{j \in J}}^{}$P(j) mathend000#

  mit J = mathend000# alle vorkommenden Index-Ausdrücke (ohne die quantifizierten Variablen)

• select mathend000# entfernen: ersetze select(a, i) mathend000# durch f_a(i) mathend000#

Für Startformel F mathend000# der Array-Logik in NNF:

Verfahren erzeugt erfüllbarkeitsäquivalente Formel F' mathend000#

mit Index-Prädikaten und uninterpretierten Funktionen.

⇒ mathend000# Betrachtung von Theorie-Kombinationen