Zusammenfassung Entscheidbarkeit

durch Automaten-Operationen sind realisierbar:

• elementare Relationen (x + y = z mathend000#)
• Quantoren und logische Verknüpfungen

Folgerungen

• zu jeder Presburger-Formel F mathend000# kann ein Automat A mathend000# konstruiert werden mit Mod(F) = Lang(A) mathend000#.
• Allgemeingültigkeit, Erfüllbarkeit, Widersprüchlichkeit von Presburger-Formel ist entscheidbar.

die Komplexität des hier angegeben Entscheidungsverfahrens ist hoch, geht das besser?