Ich bin ein Ersti bei Informatikstudium und finde es immer erstaunlich dass man auf RUclips häufig bessere Erklärungen findet als in den Vorlesungen... Tolles Video, liebe Grüße aus Wien! :)
falls Res° (K) = {{¬P, H, C}, {¬P, ¬H}, {P},{¬C}} gemeint ist, das Bild eine Folie danach erklärt es e ganz gut //////////////////////////////////////////////////////////////// wir vergleichen erst einmal 1.Klause mit 2.Klausel {¬P, H, C}, {¬P, ¬H} Merkt euch, dass alles hier mit ODER verknüpft ist, weil alles eine Klausel ist heißt ¬P v ¬P = ¬P (¬P existiert in beiden Klauseln) heißt H v ¬H = 1 (H ist in 1.Klausel, ¬H ist in 2.Klausel) es wäre unnötig ¬P zweimal aufzuschreiben, sprachlich könnte man sagen: "Theorie ist scheiße ODER Theorie ist scheiße" H kann man löschen "Ich lerne ODER Ich lerne nicht", eins ist IMMER wahr, also ist es kein Problem H zu löschen C nehmen wir mit, weil für C gibt es kein anderen C oder ¬C in der 2.Klausel also bleibt ¬P und C übrig, H ist ja gelöscht worden Lösung für 1.Klausel und 2.Klausel ist: {¬P, C} /////////////////////////////////////////////////////////////////////////////////////////////// Ergebnis vergleicht man mit 3.Klause: {¬P, C}, {P} ¬P v P = 1 also bleibt nur C übrig Ergebnis von 1.Klausel, 2.Klause und 3.Klausel: {C} //////////////////////////////////////////////////////////////// Jetzt einfach Ergebnis wieder mit 4.Klause vergleichen: {C}, {¬C} C v ¬C = 1 was eine leere Klausel entspricht //////////////////////////////////////////////////////////////// Ergebnis: Leere Klausel, also Formel unerfüllbar
Du hast mir letztes Semester in TI geholfen und jetzt deine Videos zu Logik. Ein Traum! Vielen Dank dafür! Die besten Erklärvideos zu den Themen kommen definitiv von dir.
Es muss doch irgendwas in der Didaktik von Hochschulen und Universitäten schief laufen, wenn so viele Informatik Studenten auf dein Erklärungstalent angewiesen sind.
Mir ist gerade was aufgefallen. Wenn man in der Formel eine Äquivalenz hätte, zB. x y, dann wäre das umgeformt: ((nicht_x oder y) und (nicht_y oder x)). Die beiden Disjunktionen kann ich ja wieder als Menge sehen für die Resolution. Jetzt würde sich doch automatisch ein Widerspruch ergeben, da diese beiden Disjunktionen sich ja gegenseitig auslöschen. Somit wären alle Äquivalenzen ein Widerspurch? Wo ist mein Denkfehler?
Wenn Du einen Resolutionsschritt auf die beiden Klauseln anwendest, dann kommt die Klausel (nicht x oder x) raus, bzw. die Klausel (nicht y oder y). Keine dacon ist die leere Klausel, und es lassen sich auch keine weiteren Klauseln mehr durch Resolution erzeugen. Es gibt also keinen Widerspruch. Hast Du eventuell gedacht, dass man auch für 2 Variablen gleichzeitig den Resolutionsschritt machen darf? Das ist nicht erlaubt. Es darf immer nur an einer Variable resolviert werden.
@@NLogSpace Achso, ja ich dachte es spielt keine Rolle wie viele Variablen in einem Schritt resolviert werden. Wie bei einer Funktionsgleichung z.B. Danke für die Antwort! LG
Ja genau, bei DNF funktioniert es genau so für das Gültigkeitsproblem. Aber es dreht sich alles um: Konjunktionen werden zu Disjunktionen und umgekehrt. Und wenn man die leere Klausel bekommt, dann war die Formel gültig.
"Ja, Voraussetzungen dürfen mehrfach genutzt werden 3:01 PM bei einer Resolution folgert ihr die ganze Zeit einfach weitere Fakten, die Fakten (bzw. Klauseln) die von Anfang an da waren sich also die ganze Zeit nutzbar" antwort meiner übungsleiterin^^
ich wollte mal Fragen wie das ganze aussieht, wenn man versucht eine Klausel mit sich selbst zu resolvieren oder zwei Literale gleichzeitig ? ich weiß bei letzterem, dass es nicht möglich ist, finde jedoch zu beiden Themen nirgendwo einen Beweis oder eine Erklärung dazu.
Wenn du eine Klausel mit sich selbst resolvierst, kommt die Ausgangs Klausel wieder raus, es ändert sich also nichts. z.B bei A, !A kommt A, !A wieder raus, da A resolviert mit A und !A mit !A wieder A, !A ergeben. (Hoffe das ist verständlich, ! bedeutet negation)
Gute Frage! Wenn die Formel erfüllbar ist, dann kann man das Verfahren zu Ende durchführen und erzeugt dabei nicht die leere Klausel. Alle anderen erzeugten Klauseln müssen aber durch jede erfüllende Belegung wahr gemacht werden. D.h. man könnte sich auf folgende Weise eine erfüllende Belegung bauen: 1. Falls es Klauseln gibt, die nur ein Literal enthalten, belege die Variable entsprechend. Also wenn die Klausel {A} abgeleitet wurde, setze A auf wahr. Wenn {nicht B} abgeleitet wurde, setze B auf falsch. 2. Alle anderen Variablen können beliebig belegt werden.
@@NLogSpace na ja - ob das immer geht... In einem kombinatorischen Problem müsste ein SAT -solver verschiedene teilbelegungen durchprobieren (mit backtracking und/oder restarts), bevor eine Belegung vollständig passt. Ich versteh nicht, wann und wo Resolution backtracking macht
Ja mir fällt gerade auf, dass mein Algorithmus noch nicht stimmt: man belegt erstmal die eindeutigen Variablen wie in Schritt 1. Dann wählt man eine noch nicht belegte Variable und gibt ihr einen beliebigen Wert (da die Resolution dieser Variable keinen eindeutigen Wert zugeordnet hat, gibt es eine erfüllende Belegung, egal wie man sie belegt). Mit dieser neuen Belegung setzt man jetzt die Resolution fort. Sobald keine neuen Klauseln mehr abgeleitet werden, wiederholt man den ganzen Prozess, also wieder die eindeutigen Variablen belegen und dann, sofern vorhanden, eine noch nicht belegte Variable beliebig belegen. Das wiederholt man so lange, bis alle Variablen belegt sind. Backtracking wird bei diesem Verfahren nicht notwendig. Der Aufwand steckt aber in der Resolution selbst, die kann nämlich exponentiell lange dauern.
![I.N "HALLUCINATION" | [Stray Kids : SKZ-PLAYER]](http://i.ytimg.com/vi/n5B5q1Hwt_U/mqdefault.jpg)
Ich bin ein Ersti bei Informatikstudium und finde es immer erstaunlich dass man auf RUclips häufig bessere Erklärungen findet als in den Vorlesungen... Tolles Video, liebe Grüße aus Wien! :)
Ich bin auch hier weil ich es aus den TI Folien gerade nicht so recht verstanden habe ^^. Bist du noch aktiv dran?
LG aus der Währingerstraße.
@@KingStarAlex Haha same here. Die THI-Vorlesung ist eine Katastrophe xD
@@vibes_3080 das komplette gegenteil zur tgi vorlesung 😂
@@KingStarAlex Absolut, Reichl-Janecek Kombo war genial und super zum Lernen
falls
Res° (K) = {{¬P, H, C}, {¬P, ¬H}, {P},{¬C}}
gemeint ist, das Bild eine Folie danach erklärt es e ganz gut
////////////////////////////////////////////////////////////////
wir vergleichen erst einmal 1.Klause mit 2.Klausel
{¬P, H, C}, {¬P, ¬H}
Merkt euch, dass alles hier mit ODER verknüpft ist, weil alles eine Klausel ist
heißt ¬P v ¬P = ¬P (¬P existiert in beiden Klauseln)
heißt H v ¬H = 1 (H ist in 1.Klausel, ¬H ist in 2.Klausel)
es wäre unnötig ¬P zweimal aufzuschreiben, sprachlich könnte man sagen: "Theorie ist scheiße ODER Theorie ist scheiße"
H kann man löschen "Ich lerne ODER Ich lerne nicht", eins ist IMMER wahr, also ist es kein Problem H zu löschen
C nehmen wir mit, weil für C gibt es kein anderen C oder ¬C in der 2.Klausel
also bleibt ¬P und C übrig, H ist ja gelöscht worden
Lösung für 1.Klausel und 2.Klausel ist:
{¬P, C}
///////////////////////////////////////////////////////////////////////////////////////////////
Ergebnis vergleicht man mit 3.Klause:
{¬P, C}, {P}
¬P v P = 1
also bleibt nur C übrig
Ergebnis von 1.Klausel, 2.Klause und 3.Klausel:
{C}
////////////////////////////////////////////////////////////////
Jetzt einfach Ergebnis wieder mit 4.Klause vergleichen:
{C}, {¬C}
C v ¬C = 1
was eine leere Klausel entspricht
////////////////////////////////////////////////////////////////
Ergebnis: Leere Klausel, also Formel unerfüllbar
omg in 3 Tagen Prüfung und heute erst hab ich dich entdeckt... Gott segne dich. Noch nie so schnell so viel verstanden
klasse Videoreihe! Hilft mir als Erstsemestler in Informatik enorm weiter!
Immer weiter so :)
Du hast mir letztes Semester in TI geholfen und jetzt deine Videos zu Logik. Ein Traum! Vielen Dank dafür! Die besten Erklärvideos zu den Themen kommen definitiv von dir.
die videos sind gut. schön erklärt, gutes tempo, inhalt deutlich und zusammenhängend
Richtig verständlich und detailiert erklärt. Vielen Dank!
Vielen Dank, endlich habe ich das verstanden!
Endlich voll verstanden, hoffentlich kommt es auch in der Prüfung gleich dran
Ist ne super Aufgabe für Prüfungen! Einfach die Aufgaben zu erstellen und zu korrigieren.
Großartiges Video, danke Dir.
Top 1000x Dank. Habe es mit meinem super Matheskript auf 2 Seiten nicht gecheckt, wobei es echt total simpel ist.
Ich hatte wie die Equivalenz hier funktioniert nicht ganz verstanden. Jetzt aber schon. Vielen Dank.
Hat uns sehr geholfen, vielen Dank.
Super Kanal!
Es muss doch irgendwas in der Didaktik von Hochschulen und Universitäten schief laufen, wenn so viele Informatik Studenten auf dein Erklärungstalent angewiesen sind.
Haha find ich auch..
waaaas? formale sprache ist doch eindeutig und so leicht zu verstehen :DD wofür schon beispiele geben
Sehr gutes Video!
Du bist der Beste dankkke !
Richtig gut. Nen Video zum Konpaktheitssatz wär Klasse!
geil, super hilfreich!
Sehr hilfreich, danke
Kann man ein Klausel mehrmals nutzen um zu resolvieren?
Ja
Mir ist gerade was aufgefallen. Wenn man in der Formel eine Äquivalenz hätte, zB. x y, dann wäre das umgeformt: ((nicht_x oder y) und (nicht_y oder x)). Die beiden Disjunktionen kann ich ja wieder als Menge sehen für die Resolution. Jetzt würde sich doch automatisch ein Widerspruch ergeben, da diese beiden Disjunktionen sich ja gegenseitig auslöschen. Somit wären alle Äquivalenzen ein Widerspurch? Wo ist mein Denkfehler?
Wenn Du einen Resolutionsschritt auf die beiden Klauseln anwendest, dann kommt die Klausel (nicht x oder x) raus, bzw. die Klausel (nicht y oder y). Keine dacon ist die leere Klausel, und es lassen sich auch keine weiteren Klauseln mehr durch Resolution erzeugen. Es gibt also keinen Widerspruch.
Hast Du eventuell gedacht, dass man auch für 2 Variablen gleichzeitig den Resolutionsschritt machen darf? Das ist nicht erlaubt. Es darf immer nur an einer Variable resolviert werden.
@@NLogSpace Achso, ja ich dachte es spielt keine Rolle wie viele Variablen in einem Schritt resolviert werden. Wie bei einer Funktionsgleichung z.B. Danke für die Antwort! LG
herrlich erklärt
Tolles Video! Funktioniert das bei der DNF einer Funktion genau so?
Ja genau, bei DNF funktioniert es genau so für das Gültigkeitsproblem. Aber es dreht sich alles um: Konjunktionen werden zu Disjunktionen und umgekehrt. Und wenn man die leere Klausel bekommt, dann war die Formel gültig.
man muss nicht alle klauseln benutzen oder?
darf man Klauseln mehrfach für resolutionsschritte nutzen?
"Ja, Voraussetzungen dürfen mehrfach genutzt werden
3:01 PM
bei einer Resolution folgert ihr die ganze Zeit einfach weitere Fakten, die Fakten (bzw. Klauseln) die von Anfang an da waren sich also die ganze Zeit nutzbar"
antwort meiner übungsleiterin^^
Sehr gutes Video
bro bis jetzt rettest du mein studium...
ich wollte mal Fragen wie das ganze aussieht, wenn man versucht eine Klausel mit sich selbst zu resolvieren oder zwei Literale gleichzeitig ? ich weiß bei letzterem, dass es nicht möglich ist, finde jedoch zu beiden Themen nirgendwo einen Beweis oder eine Erklärung dazu.
Wenn du eine Klausel mit sich selbst resolvierst, kommt die Ausgangs Klausel wieder raus, es ändert sich also nichts. z.B bei A, !A kommt A, !A wieder raus, da A resolviert mit A und !A mit !A wieder A, !A ergeben. (Hoffe das ist verständlich, ! bedeutet negation)
Wie komm ich denn bei einer erfüllbaren Formel mit vielen Resolutionschritten zur Variablenbelegung?
Gute Frage! Wenn die Formel erfüllbar ist, dann kann man das Verfahren zu Ende durchführen und erzeugt dabei nicht die leere Klausel. Alle anderen erzeugten Klauseln müssen aber durch jede erfüllende Belegung wahr gemacht werden. D.h. man könnte sich auf folgende Weise eine erfüllende Belegung bauen:
1. Falls es Klauseln gibt, die nur ein Literal enthalten, belege die Variable entsprechend. Also wenn die Klausel {A} abgeleitet wurde, setze A auf wahr. Wenn {nicht B} abgeleitet wurde, setze B auf falsch.
2. Alle anderen Variablen können beliebig belegt werden.
@@NLogSpace na ja - ob das immer geht... In einem kombinatorischen Problem müsste ein SAT -solver verschiedene teilbelegungen durchprobieren (mit backtracking und/oder restarts), bevor eine Belegung vollständig passt. Ich versteh nicht, wann und wo Resolution backtracking macht
Ja mir fällt gerade auf, dass mein Algorithmus noch nicht stimmt: man belegt erstmal die eindeutigen Variablen wie in Schritt 1. Dann wählt man eine noch nicht belegte Variable und gibt ihr einen beliebigen Wert (da die Resolution dieser Variable keinen eindeutigen Wert zugeordnet hat, gibt es eine erfüllende Belegung, egal wie man sie belegt). Mit dieser neuen Belegung setzt man jetzt die Resolution fort. Sobald keine neuen Klauseln mehr abgeleitet werden, wiederholt man den ganzen Prozess, also wieder die eindeutigen Variablen belegen und dann, sofern vorhanden, eine noch nicht belegte Variable beliebig belegen. Das wiederholt man so lange, bis alle Variablen belegt sind.
Backtracking wird bei diesem Verfahren nicht notwendig. Der Aufwand steckt aber in der Resolution selbst, die kann nämlich exponentiell lange dauern.
@@NLogSpace nun ja - im richtigen Leben würde man ja auch mit subsumption arbeiten und so das Wachstum ein bisschen einfangen
Der Link geht leider nicht
Oh sorry, da war ich mit den Videos schneller als mit den Aufgaben. Ich versuche die demnächst fertig zu machen!