Zusammenfassung Entscheidbarkeit

durch Automaten-Operationen sind realisierbar:

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

Folgerungen

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

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