Warum führt man bei der Delta-Expansion immer neue Konstanten ein?
Danke!

Ich schätze du sprichst von der Prädikatenlogik, genauer gesagt von dem dort eingesetzten Beweisverfahren -> Tableau-Kalkül. Dort werden die "zusätzlichen" Schlussregel/Inferenzregel "Gamma-Regel" und "Delta-Regel" verwendet.

Mit der Gamma-Regel wird ein Allquantor (\/x.F) bzw. ein negierter Existenzquantor eliminiert, indem einfach x durch eine neue Variable y (oder ein geschlossener Term) substituiert wird. (Die Ersetzung muss hierbei Kollisionsfrei erfolgen).

Die Delta-Regel hingegen definiert den Umgang mit Existenzaussagen. Hierbei wird die betroffene Variable x skolemisiert, …
Variante 1 [LOS Folie 9-2]:
… indem sie durch eine Konstante p ersetzt wird. Hierbei ist p ein neues Parametersymbol, das in F noch nicht vorkommt.

Variante 2 [LOS Folie 9-13].
… indem sie durch einen Term f(x1,…,xn) ersetzt wird. Hierbei ist f ein neues Funktionssymbol und x1,…,xn sind freie Variablen von F.

Dazu zwei praktische Beispiele:

Fall 1) Eine einfache Existenzaussage F wird ja genau dann wahr, wenn für eine Belegung für x existiert, die F wahr werden lässt. Der Wert von x ist nicht davon abhängig, wie wir die anderen in F vorkommenden Variablen belegen. Von daher können wir x einfach durch ein neues Konstantensymbol das noch nicht in F enthalten ist ersetzten. Damit erhalten wir eine Formel ohne Existenzquantor die erfüllbarkeitsäquivalent zur ursprünglichen Formel ist.

Fall 2) Bei einer Formel F der Art Vx1…Vxn Ex.F ist es etwas komplizierter. Eine solche Formel wird genau dann wahr, wenn für alle Wertkombinationen x1,…xn eine Belegung für x existiert, die F wahr werden lässt. Anders als im ersten Fall, kann x nicht einfach ersetzt werden, da ja die Belegung von x von den konkreten x1, …, xn abhängt. Wenn aber für jede Wertekombination x1,…,xn eine Belegung für x existiert, dann lässt sich der Wert von x durch eine n-stellige Funktion f berechnen. Genau diese f(x1,…xn) können wir dann gegen x ersetzten, um den Existenzquantor zu eliminieren und eine erfüllbarkeitsäquivalente Formel zu erhalten.

Das Ziel der Übung bzw. der Regeln ist also die Quantoren zu eliminieren…
Um ein prädikatenlogisches Tableau abzuschließen, muss man diese Regeln jedoch auch mehrmals anwenden. Dies führt bei der Delta-Regel in der Folge zu immer neuen Teilformeln mit jeweils verschiedenen Konstanten (siehe LOS-Folie 9-6)

Hat das alle Klarheiten beseitigt?
Falls du noch weitere Fragen hast nur zu - bis Montag ist ja noch etwas Zeit ;)
greetz

[Alle Angaben ohne Gewähr]
[Quellen: Theoretische Informatik, Dirk Hoffmann, Hanser Verlag, S.114ff]

Alles klar!
vielen vielen Dank!

Ich habe ja noch eine Frage.
Zwar,Wenn esmehrere Delta- Expansionen gab, welche von den neu eingeführten Konstanten wird dann für die Gamma- Expansion benutzt?
Danke!

Warum führt man bei der  Delta-Expansion immer neue Konstanten ein?
Danke!

ich versuche mal etwas sprachlicher….

Wenn du bei der Delta-Exp. das x durch etwas ersetzt, dann weißt du, dass ein x existiert, das die Formel wahr
macht. Du weißt aber nicht, in wie weit dieses x von etwas andrem abhängig ist.

wenn du  die Variable x also nicht durch einen *neuen* Parameter ersetzt, sondern durch einen der schon mal aufgetreten ist, dann sagst du im Prinzip, dass es ein x  mit speziellen Eigenschaften  existiert, dass
dann - mit diesen speziellen Eigenschaften - die Formel wahr macht.
Dann steckst du doch Wissen in den Tableau-Beweis, das du aber gar nicht hast!

Zu der 2. Frage: "Zwar,Wenn esmehrere Delta- Expansionen gab, welche von den neu eingeführten Konstanten wird dann für die Gamma- Expansion benutzt?"

So wie ich dich verstanden habe, hast du mehrere Delta-Exp. durchgeführt und es bleiben nur noch Gamma-Formeln übrig?
Da wir hier jetzt nur noch universelle Formel haben, können wir dann die Variable beliebig durch irgendeine Konstante ersetzen, mit dem Ziel: Abgeschlossenheit.
Wenn du z.b. -P(a) durch Delta-Exp. erzeugt hast und es liegt noch A.x P(x) vor, dann ersetzt du natürlich das x durch a, damit du zum Abschluss kommst