Klausur Konfluenz und Terminierung

Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.

Klausur Konfluenz und Terminierung
Ich hänge aktuell bei der TES Aufgaben.

“Ist dieses System terminierend? Geben Sie einen Beweis mittels Polynomordnungen oder
ein Gegenbeispiel an.”

Das ganze ist eigentlich nicht kompliziert. Ich hänge aber jedes mal aufs neue an der “Polynomwahl” mit denen ich die Funktionssymbole ersetzen will.
Gibt es dafür einen Trick, wie man da leichter draufkommt?


Ich würde die Übungen nochmal selber durchmachen und mich an den Altklausuren versuchen, irgenwann sieht man was man versuchen muss. Gloin geht ohne großes Verständnis für die Theorie dahinter.


In der Regel bietet es sich an, mit möglichst einfachen Polynomen zu beginnen, also etwa x+y oder xy. Wenn die nicht funktionieren, etwa weil auf beiden Seiten der gleiche Term herauskommt, dann muss man sich ein paar Modifikationen überlegen, die die linke Seite strikt größer machen. Das ist dann in der Regel so etwas wie “ersetze x durch x+1” oder "ersetze y durch 2y".