Resolution < Prädikatenlogik < Logik < Logik+Mengenlehre < Hochschule < Mathe < Vorhilfe
|
| Status: |
(Frage) reagiert/warte auf Reaktion  | | Datum: | 20:58 Do 21.08.2008 | | Autor: | Rudy |
Hi,
hätte ein Problem zur Resolution.
Wenn ein [mm]\forall x[/mm] vorkommt, dann habe ich ja eine Klauselmenge, die sehr groß wäre, denn für jedes vorkommen von x steht ein Element aus der Signatur drin.
Um nun zu zeigen, dass [mm] \Box [/mm] drin ist, muss ich nur die Resolution anwenden auf einen Teil der Klauselmenge.
Wenn die Formel z.b. so lautet
[mm]\forall x (Px \wedge \neg Pfx)[/mm]
dann habe ich als Klauselmenge [mm]\left\{Pt\right\}, \left\{\neg Pfs\right\}[/mm] wobei [mm]t,s \in T_0(S)[/mm] und [mm]T_0(S) = \left\{c, fc, ffc, ..\right\} [/mm]
Wenn man nun die Klauseln aufschreiben würde, dann würde man sowas bekommen:
[mm]\left\{Pc\right\}, \left\{\neg Pfc\right\}, \left\{Pfc\right\}, \left\{\neg Pffc\right\}...[/mm]
mit Resolution wäre dies doch unerfüllbar oder?
denn hieraus bekäme ich die [mm] \Box[/mm] :
[mm] \left\{\neg Pfc\right\}, \left\{Pfc\right\}[/mm]
Aber warum? [mm]Px[/mm] ist doch nicht unebedingt das selbe wie [mm]Pfx[/mm].
Mein anderes Problem ist:
Wenn [mm] \varphi [/mm] Allgemeingültig sein soll, darf man dann mit Resolution zeigen, dass [mm] \neg \varphi[/mm] unerfüllbar ist? Oder darf man dies nicht machen?
Und mein drittes Problem. Mit Herbrand-Modell kann man ein Modell angeben, womit ein Satz erfüllbar ist. Bei meinem obrigen Beispiel, wäre doch für x=c aus [mm]T_0(S)[/mm] erfüllbar. Aber mit Resolution habe ich doch gezeigt, dass dies unerfüllbar ist.
erfüllbar ist doch, wenn es ein Modell gibt, der diesen Satz erfüllbar macht.
Ich weiß, es sind viele Fragen.
Vielen Dank schonmal.
|
|
| |
|
| Status: |
(Mitteilung) Reaktion unnötig  | | Datum: | 02:05 Fr 22.08.2008 | | Autor: | Rudy |
Zum Großteil haben sich meine Fragen erledigt:
Meine erkenntnisse dazu:
> Mein anderes Problem ist:
> Wenn [mm]\varphi[/mm] Allgemeingültig sein soll, darf man dann mit
> Resolution zeigen, dass [mm]\neg \varphi[/mm] unerfüllbar ist? Oder
> darf man dies nicht machen?
Ja darf man!
> Und mein drittes Problem. Mit Herbrand-Modell kann man ein
> Modell angeben, womit ein Satz erfüllbar ist. Bei meinem
> obrigen Beispiel, wäre doch für x=c aus [mm]T_0(S)[/mm] erfüllbar.
> Aber mit Resolution habe ich doch gezeigt, dass dies
> unerfüllbar ist.
>
> erfüllbar ist doch, wenn es ein Modell gibt, der diesen
> Satz erfüllbar macht.
Hatte anscheinend das Herbrand-Modell nicht so ganz verstanden.
Es muss für die komplette Trägermenge gelten, dann ist es erfüllbar! D.h. es müsste für c, fc, ffc usw. gelten (und dies gleichzeitg?!?).
|
|
|
|
