Folgerungen aus Unentscheidbarkeit

Suche nach (effizienten) Algorithmen für Spezialfälle

(die trotzdem ausreichen, um interessante Anwendungsprobleme zu modellieren)

• Einschränkung der Signatur (Bsp: keine F.-S., nur einstellige F.-S, nur einstellige Rel.-S.)
• Einschränkung der Formelsyntax
  • nur bestimmte Quantoren, nur an bestimmten Stellen

    (im einfachsten Fall: ganz außen existentiell)

  • nur bestimmte Verknüpfungen (Bsp: nur durch ∧)
• Einschränkung auf Theorien von gegebenen Strukturen

  Bsp: F∈Th($\mathbb {N}$, 0, +)? Theorie der ganzen Zahlen mit Addition