Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Lösungen der Übungen
Die Lösungen der Übungsblätter sind in dem “Übungsblätter Kumulativ”-Dokument nicht komplett vollständig.
Zu manchen Aufgaben wie beispielsweise Problem 8.2 gibt es garkeine Lösung. Da ich in Bezug auf Natural Deduction
jedoch noch einige Probleme habe, wäre es gut dort eine Lösung zu haben. Es wäre super wenn diese Lösung noch ergänzt werden könnte.
Stimmt, ja. Ich hab mal entsprechend die natural deduction lösungen schonmal hochgeladen, braucht ihr die anderen (tableau/resolution) auch noch unbedingt? Texen kostet halt doch etwas zeit… :3
War die hochgeladene Lösung speziell zu 8.2? In dem assignments.pdf kann ich nämlich nichts finden, evtl. hab ich die Lösung auch nur übersehen.
Also ich brauche die Lösungen für Tableau/Resolution nicht. Vielen Dank schonmal
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]…