[LOS] Aufgabeblatt 5 Nr. 1 (Aufgabe 9.1Script 1) Predikatenlogisches Tableau - Druckversion
+- FB18.de - Das Informatikforum ( /mybb ) +-- Forum: Diplom Informatik ( /forumdisplay.php?fid=114 ) +--- Forum: Theoretische Informatik (HS) ( /forumdisplay.php?fid=75 ) +--- Thema: [LOS] Aufgabeblatt 5 Nr. 1 (Aufgabe 9.1Script 1) Predikatenlogisches Tableau ( /showthread.php?tid=8878 ) |
[LOS] Aufgabeblatt 5 Nr. 1 (Aufgabe 9.1Script 1) Predikatenlogisches Tableau - 3becker - 15.09.2007 17:04 Wir glauben das dieser Beweis Falsch ist. Kann uns jemand den Denkfehler aufzigen? (Oder sagen das wir doch richtig lagen):
Code:
!(Ax Ey Az Ew (R(w,z) -> R(x,y)))
RE: [LOS] Aufgabeblatt 5 Nr. 1 (Aufgabe 9.1Script 1) Predikatenlogisches Tableau - georg - 15.09.2007 17:58 Dass die oberste Formel keine Kontradiktion ist, sieht man schon am Modell mit Universum {1,2} und mit R als {(1,2)}. Der Fehler ist, dass bei der Gamma-Expansion ein bestimmter geschlossener Term eingesetzt werden muss und keine Term-Variable, deren genauer Inhalt erst später definiert wird (im Prinzip also dort, wo ihr einen Kommentar machen musstet um euren Schritt zu begründen ). Das liegt daran, dass bei diesem Vorgehen ja die Belegung der durch Allquantoren gebundenen Variablen in bestimmter Weise (in dem Fall durch die Regel t2=c und t1=d) von der Belegung der durch Existenzquantoren gebundenen abhängt. Ihr habt also nur die Belegungen betrachtet, für die y=x und w=z ist, womit die oberste Formel nicht erfüllbar ist. Da aber eine Formel u.U. durch ganz andere Belegungen erfüllt werden kann (wo eben diese Abhängigkeit nicht gegeben ist), sind solche Schritte im Tableau nicht erlaubt. Also: Statt Termvariablen immer konkrete geschlossene Terme in der Gamma-Expansion verwenden. RE: [LOS] Aufgabeblatt 5 Nr. 1 (Aufgabe 9.1Script 1) Predikatenlogisches Tableau - Sven Port - 15.09.2007 18:06 gibt es keinen tableau-beweis, d.h.: das initiale tableau ist folgendes: wenn man nun berücksichtigt, dass:
kann man ziemlich schnell sehen, dass das tableau nicht abgeschlossen werden kann. RE: [LOS] Aufgabeblatt 5 Nr. 1 (Aufgabe 9.1Script 1) Predikatenlogisches Tableau - Sven Port - 15.09.2007 18:07 ups, zu spät... RE: [LOS] Aufgabeblatt 5 Nr. 1 (Aufgabe 9.1Script 1) Predikatenlogisches Tableau - georg - 15.09.2007 18:18
Sven Port schrieb:
wenn man nun berücksichtigt, dass:
RE: [LOS] Aufgabeblatt 5 Nr. 1 (Aufgabe 9.1Script 1) Predikatenlogisches Tableau - queery - 16.09.2007 09:19 Das mit den Variablen hatten wir gemacht aus der Überlegung, dass wir ja eigentlich die Quantorenreihenfolge ohne das es stört verändern können und so sozusagen die Universalexpansion nach den anderen zwei machen könnten. Heist das denn jetzt, wenn ich so ein Tableau Beweis hab (s.u.) müsste ich sozusagen begründen, warum ich die Gamma-Variable auf a beschränken kann?
Code:
!(Ax [(P(x) --> Q(x)) & P(a)] --> Q(a))
RE: [LOS] Aufgabeblatt 5 Nr. 1 (Aufgabe 9.1Script 1) Predikatenlogisches Tableau - Anonymer User - 16.09.2007 11:29 Huch?! Nein, nein, Quantoren koennt ihr nicht einfach beliebig vertauschen! Beispiel: Fuer jede natuerliche Zahl n gibt es eine natuerliche Zahl m mit n < m Formal: A n E m <(n,m) (z.B. m := n + 1) Aber andersherum E m A n <(n,m) macht das keinen Sinn (es gibt eine natuerlich Zahl, die groesser ist als alle natuerlichen Zahlen - das geht nicht). Froehliche Gruesse RE: [LOS] Aufgabeblatt 5 Nr. 1 (Aufgabe 9.1Script 1) Predikatenlogisches Tableau - georg - 16.09.2007 14:47
queery schrieb:
Das mit den Variablen hatten wir gemacht aus der Überlegung, dass wir ja eigentlich die Quantorenreihenfolge ohne das es stört verändern können und so sozusagen die Universalexpansion nach den anderen zwei machen könnten.
Zitat:
Heist das denn jetzt, wenn ich so ein Tableau Beweis hab (s.u.) müsste ich sozusagen begründen, warum ich die Gamma-Variable auf a beschränken kann?
RE: [LOS] Aufgabeblatt 5 Nr. 1 (Aufgabe 9.1Script 1) Predikatenlogisches Tableau - 3becker - 17.09.2007 10:51 Hallo, ist das jetzt als Lösung für die Aufgabe unter Zuhilfenahme von "Free-Variable Semanic Tableaux" (S. 166 . Fitting, First-Order and Automated Theorem Proving)?
Code:
!(Ax Ey Az Ew (R(w,z) -> R(x,y)))
RE: [LOS] Aufgabeblatt 5 Nr. 1 (Aufgabe 9.1Script 1) Predikatenlogisches Tableau - Anonymer User - 18.09.2007 11:55 Hilfee, also ich hab bei Aufgabe 9.1 !(Ax Ey Az Ew (R(w,z) -> R(x,y))) immer noch nicht verstanden woran man sieht das es kein Tableau Beweis für gibt. Kann mir jemand den Unterschied zwischen gamma und delta Expansion erklären? Bei der delta Expansion wird ein neuer Parameter eingeführt,der nicht in der Formelmenge vorhanden ist (zB. a,b,c...?) Die gamma Expansion fügt einen neuen geschlossenen Term in die Gleichung ein? (zB. t1,t2..? wobei im Skript bei einigen gamma expansionen auch einfach nur (a,b,c,d..) eingefügt wurden. Verwirrt. Hilfe! RE: [LOS] Aufgabeblatt 5 Nr. 1 (Aufgabe 9.1Script 1) Predikatenlogisches Tableau - Anonymer User - 18.09.2007 12:08 Ist es richtig, das man erkennen kann das es kein tableau beweis für die obige formel gibt, weil man2 delta und 2 gamma expansionen ausführen muss und somit bei (R(w,z)->R(x,y)) zwei Terme entstehen, die nicht zum Abschluss führen können? |