Hi Dennis, ein Kollege und ich bräuchten doch die Lösung von 10.2 und 10.3 aus den Assignments. Ausserdem brauchen wir Problem 4.3 (mit Resolution) aus der Mockexam. Wir waren uns an paar Stellen nicht ganz sicher und wollen sicher verifizieren. Uns würde das auch nicht stören wenn du das mit plain ASCII Zeichen machst.
Lösung zu Mockexam 4.3 findet ihr hier: https://fsi.cs.fau.de/forum/thread/15579-Probeklausur
Und hier mein Vorschlag zu den Assignments ohne Gewähr auf Korrektheit:
edit: Anwendung von Conjunctive Normal Form Calculus (slides p. 461):
2 „Gefällt mir“
Bei deiner Korrektur stimmt nicht, dass da auf einmal f_n(a,b) steht, denn in der CNF^1 Regel steht, dass f_n von Variablen abhängt, nicht Konstanten (a,b sind Konstanten).
EDIT: alles was hier mal stand ist erstmal nicht wahr, da deine Lösung eig. meiner entspricht.
Ah richtig, dann müsste doch die obere Lösung stimmen und die Buchstaben mit Strich sind 0-stellige Funktionen?
An sich ja, aber dann kannst du glaube ich nicht mehr resolvieren, denn Konstanten kann man nicht miteinander unifizieren.
Was jetzt genau dann bei dir (oder in meiner Überlegung) falsch ist, weiß ich nicht, aber ich habe bei meiner Lösung die Umwandlung der exist in forall anders gemacht und trotzdem quasi die gleiche (meiner Meinung nach korrekte) Lösung hier:
Wie ist es eigentlich bei 10.3…?
Im Lösungsvorschlag von ThiloK
müsste man doch in der vorletzten Zeile:" \forall Y.P(Y)^F " dann mit einer 0-Stelligen Funktion substituieren (Slides F449). Dann würde man ja auf folgende Zeile kommen…
Jetzt müsste man doch f_1 mit Z gleichbringen. Nun sind aber f_1 und Z auf den ersten Blick zwei Paar Schuhe. f_1 ist eine Skolem Konstante (Slides F421) und Z ein Term (siehe Lemma 2.24 auf F430 - zugegeben ein sehr kleiner Term). Und da Terme nach Definition 2.3 (Slides 422) \in wff_iota(\Sigma_iota) sind und 
müsste ich doch eigentlich ganz am Anfang (oder auch im nachhinein?) anstatt mit [Z/X] direkt mit [f_1()/X] substituieren damit ich auf den Nagel komme …oder?
Edit:
Mir ist noch was aufgefallen in der Lösung von ThiloK
Ich glaube die Umformung von Zeile 4 auf Zeile 5 ist nicht erlaubt. Deshalb ist ThiloK dazu gezwungen Skolem Operatoren einzusetzen und tyr nicht. Um das T zum F zu switchen muss die negation ganz Vorne sein (siehe Regeln Slide 360) und es gilt ∀X.¬A≠¬∀X.A. Z.b. „Alle sind nicht angekommen“ ≠ „Nicht alle sind angekommen“
Meiner Meinung nach hast du recht.
Aber siehe die generalized cut rule vom free variable Tableaux: man kann hier eine Substitution, genauer diese hier: [f_1()/Z], finden, die uns den „Nagel“ bringt.
Allgemein finde ich es hier wichtig, zu sagen, ob man free variable tableaux oder first oder standard tableaux macht…
Gibt es da vlt eine Musterloesung von Offizieller Seite? Wenn nicht wuerde ich mal darum bitten:D
Ich werf mal die Übungsgruppen in den Raum, ich weiß ehrlich nicht ob ich die woche noch dazu komm da lösungen zu texen (allein die formatierung ist da halt echt aufwendig), aber ich führ sie gerne vor 
Wenn jemand morgen mitschreiben möchte o.ä. kann man das natürlich auch gerne tun und verbreiten 
Ich würde auch sehr freundlich darum bitten, denn es können nicht alle Dienstags rein kommen (wie ich) und wir bräuchten denke ich alle eine Lösung auf die wir zurückgreifen können.
Na gut, wenn bedarf ist muss ich wohl - ich versuch mich morgen drum zu kümmern
resolution und tableau für blatt 8 online
1 „Gefällt mir“
Lösungen für Blatt 10 jetzt auch online
1 „Gefällt mir“
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:
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]…
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…
Generelle Frage: kann es sein, dass es manchmal gar nicht notwendig ist zu skolemiesieren? Wie hier für Aufgabe 10.2…
Edit: Ach! mir fällt gerade auf das ist ein illegaler Move von Zeile 1 auf Zeile 2. Sooorrrryyyy
Gut, das erklärt einiges <_< Danke! Dann hier also noch mal die korrekte Umformung für alle:
1 „Gefällt mir“
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
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 
Ah, sehr gut, dann bin ich jetzt auch weniger von der Frage an sich verwirrt 