Not logged in. · Lost password · Register

Page:  previous  1  2 
Jazzpirate
Member since Oct 2016
803 posts
In reply to post ID 155028
Na gut, wenn bedarf ist muss ich wohl - ich versuch mich morgen drum zu kümmern ;)
Jazzpirate
Member since Oct 2016
803 posts
+1 Fertu
resolution und tableau für blatt 8 online
Jazzpirate
Member since Oct 2016
803 posts
+1 Fertu
Lösungen für Blatt 10 jetzt auch online
ThiloK
Member since Oct 2014
59 posts
Jetzt habe ich trotzdem noch mal eine Frage zur 10.2 (Resolution). Wenn ich den CNF^1 ganz formal durchführe, komme ich zu folgender Substitution, wobei A die gegebene Formel ist:

[Image: https://img3.picload.org/image/daggogdr/bildschirmfoto2018-02-07um10.2.png]
Edit 2: falsch, korrekte Umformung siehe hier.

Laut Musterlösung wird das Y mit f(X) substituiert, aber in Schritt 3 habe ich doch eine Formel der Form \forall X. A^T, was nach Regel auf Slide 461 zu [Z/X]A ausgewertet wird. Diese Art der Substitution hätte ich erst bei Schritt 5 erwartet. Habe ich da einen Denkfehler gemacht bzw. falsch umgeformt?

Edit: Oder dreht das F in Zeile 1 direkt alle Quantoren um zu \forall X. \exists Y. \forall Z. \forall W. ~A^T ?
Dann komme ich auch auf die Substitution [f(X)/Y]...
This post was edited 2 times, last on 2018-02-07, 11:16 by ThiloK.
Jazzpirate
Member since Oct 2016
803 posts
Edit: Oder dreht das F in Zeile 1 direkt alle Quantoren um zu \forall X. \exists Y. \forall Z. \forall W. ~A^T ?
Ja, unbedingt, sonst ist ja die Formel nicht mehr logisch äquivalent! Oder alternativ, du darfst das negationszeichen dass du in der zweiten Zeile einführst nur direkt hinter das "\forall X" packen.

Was du im prinzip machst ist:
\neg \exists X\forall  Y\exists Z\exists W...
= \forall X \neg\forall Y\exists Z\exists W...
= \forall X\exists Y\neg\exists Z\exists W...
= \forall X\existsY\forall Z\neg\exists W...
Fuxicus
Member since Apr 2017
47 posts
In reply to post #19
Generelle Frage: kann es sein, dass es manchmal gar nicht notwendig ist zu skolemiesieren? Wie hier für Aufgabe 10.2...
[Image: https://img2.picload.org/image/daggodai/blaablaa.png]

Edit: Ach! mir fällt gerade auf das ist ein illegaler Move von Zeile 1 auf Zeile 2. Sooorrrryyyy
This post was edited on 2018-02-07, 10:04 by Fuxicus.
ThiloK
Member since Oct 2014
59 posts
+1 Fuxicus
Quote by Jazzpirate:
Oder alternativ, du darfst das negationszeichen dass du in der zweiten Zeile einführst nur direkt hinter das "\forall X" packen.

Gut, das erklärt einiges <_< Danke! Dann hier also noch mal die korrekte Umformung für alle:

[Image: https://img1.picload.org/image/dagglcol/bildschirmfoto2018-02-07um12.0.png]
Jazzpirate
Member since Oct 2016
803 posts
Hmm, deinen wechsel zwischen T und F und negationen finde ich extrem verwirrend. Es ist nicht falsch was da passiert, aber mir ist nicht ganz klar, warum du das so augenscheinlich kompliziert machst...

ist das der versuch, das absolut rigoros und schritt-für-schritt nach den regeln für den CNF-algorithmus zu machen? Ich sollte in dem Fall nämlich deutlich darauf hinweisen, dass das so durchexorziert extrem zeitaufwendig aussieht und ihr euch vermutlich nicht unbedingt einen Gefallen damit tut wenn ihr so vorgeht.

...außer natürlich es geht nur darum den algorithmus zu verstehen, dann befürworte ich das absolut :)
ThiloK
Member since Oct 2014
59 posts
Quote by Jazzpirate:
ist das der versuch, das absolut rigoros und schritt-für-schritt nach den regeln für den CNF-algorithmus zu machen?

Ja genau, habe versucht die Schritte nachzuvollziehen und zu verstehen, was der Algorithmus da eigentlich tut. In der Klausur würde ich das natürlich in einem Schritt machen ;)
Jazzpirate
Member since Oct 2016
803 posts
Ah, sehr gut, dann bin ich jetzt auch weniger von der Frage an sich verwirrt :D
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Page:  previous  1  2 
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen