Automatische Terminations-Analyse

• die Menge {R | SN(→_R)} ist nicht entscheidbar,

  (Beweis: Reduktion vom Halteproblem: Simulation der Rechnung einer TM, mit zusätzlicher Betrachtung ungültiger Konfigurationskodierungen)

• wegen der großen praktischen Bedeutung in der Software-Verifikation wünscht man korrekte partielle Verfahren: diese antworten auf Frage SN(R)

  mit: Ja, Nein (beides muß stimmen) oder Weißnicht.

• Wettbewerb für Implementierungen solcher Verfahren: Intl. Termination Competition (seit 2003),

  mit Termination Problem Data Base (TPDB) http://termination-portal.org/