Wie und warum Hilft uns das Königs Lemma bei der Termination des Klauselform-Algorithmus?

Das ganze lässt sich auf Smullyans Ballaufgabe zurückführen, die sich im Königs Lemma beweisen lässt. Dabei entspricht jede Klausel einem Ball, wobei der Rang dieser Formel der Nummer auf dem Ball entspricht. Bei einer [Latex]$\beta$[/Latex]-Formel wäre das also der Rang dieser Formel. Nun wird diese Formel geteilt in [Latex]$\beta_1$[/Latex] und [Latex]$\beta_2$[/Latex]. Diese beiden Formeln entsprechen zwei neuen Bällen, die einen echt kleineren Rang haben. Der Rest wird in Smullyans Ballaufgabe erklärt.

Wir wollen doch das eine Verfahren Terminiert wissen aber das wir durch unterschiedliche Umwandlungen zur Termination gelangen können.
Ist es so das einer dieser wege Unendlich sein kann? Oder warum brauchen wir das Königs-Lemma? Diese sagt doch nur das ein endliche verzwiegter Baum ein unendlichen Pfad haben kann? Was soll der unendliche Pfad in der Ball Aufgabe sein?

Was soll der unendliche Pfad in der Ball Aufgabe sein?

Dort gibt es keinen, weshalb du ja zeigen kannst, dass das Verfahren stark terminiert. Wenn es nicht terminieren würde, müsste es ja mind. einen nicht endlichen Zweig geben, was dir Königs Lemma sagt.

Also sagen wir das das Königs Lemma nicht gilt!?!? und wir deswegen sagen das der Klauselform-Algorithmus stark terminiert???

Also sagen wir das das Königs Lemma nicht gilt!?!? und wir deswegen sagen das der Klauselform-Algorithmus stark terminiert???

Das ganze sieht doch nach einem Widerspruchsbeweis aus:
Gäbe es unendlich viele erreichbare Konfigurationen in einer Berechnung, so gäbe es, wegen Königs Lemma,
auch einen unendlichen Berechnungspfad (im lokal endlichen Baum der (Sub-)Terme, Smullyans Bälle).

Da es Letzeres wegen der kleiner werdenden Ränge nicht geben kann, gibt es also auch keine nicht terminierende Rechnung, und das Verfahren terminiert.

So ähnlich dürfte die Argumentation wohl sein, oder? (Ich war nicht in dieser Vorlesung…)