Prof. Markus
Prof. Markus
  • 128
  • 134 400
Logik höherer Ordnung (und Datalog)
Bisher haben wir Prädikatenlogik *erster Stufe* kennengelernt. In diesem Video erkläre ich kurz, was Prädikatenlogik zweiter Stufe ist und wozu diese Erweiterung nützlich sein kann. Dabei sehen wir auch, wie man durch diese Erweiterung auch Datalog-Programme wieder natürlich als logische Formeln auffassen kann, für die wir bei der Anfragebeantwortung ein logisches Auswertungsproblem (Model Checking) auf einer endlichen Interpretation (Datenbank) lösen.
► Playliste für diesen Videokurs: ua-cam.com/play/PLz7XhF-sAU8z4FtL7V9uefCXzW9Z9rk5c.html
► Vorlesungsfolien zum Download: iccl.inf.tu-dresden.de/web/TheoLog2021 (22. Vorlesung)
► Aktuelle und frühere Versionen der Vorlesung: iccl.inf.tu-dresden.de/web/TheoLog
► Fehler gefunden? Issues melden auf github: github.com/knowsys/TheoLog
Переглядів: 794

Відео

Auswertung von Datalog
Переглядів 5333 роки тому
Datalog-Programme lassen sich recht einfach direkt auswerten, indem man solange Regeln anwendet, bis keine neuen Fakten mehr abgeleitet werden können. Diese Idee liefert einen ersten (wenn auch unoptimierten) Algorithmus, den man als eine Variante der prädikatenlogischen Resolution auffassen kann. Die so ermittelten Schlüsse kann man sich auch gut mit Hilfe von Ableitungsbäumen veranschaulichen...
Rekursion, Prädikatenlogik und Datalog
Переглядів 4293 роки тому
Rekursion ist ein wichtiges Feature in Abfragesprachen moderner Datenbanken, das aber in Prädikatenlogik nicht ausgedrückt werden kann. Oder geht das nicht vielleicht doch? Die Diskussion dieser Frage führt uns den Unterschied zwischen Auwertungsproblem (Model Checking) und logischen Schließen (Entailment) noch einmal vor Augen. Am Ende definieren wir Datalog, und zwar zunächst als Fragment der...
Prädikatenlogik und Datenbanken (2)
Переглядів 2713 роки тому
Wir wollen noch zeigen, dass das Auswertungsproblem der Prädikatenlogik (und damit auch die Anfragebeantwortung in Datenbanken) PSpace-vollständig sind, was man leicht durch Reduktion von TrueQBF zeigen kann. Zum Schluss schauen wir noch einmal auf die Grenzen der Ausdrucksstärke von Prädikatenlogik als Anfragesprache. ► Playliste für diesen Videokurs: ua-cam.com/play/PLz7XhF-sAU8z4FtL7V9uefCXz...
Prädikatenlogik und Datenbanken (1)
Переглядів 4113 роки тому
Prädikatenlogische Formeln und (endliche) Interpretationen entsprechen Datenbankanfragen und Datenbankinstanzen. Aus dieser Beobachtung kann man einige Einsichten ableiten, zum Beispiel dass Anfragebeantwortung viel mit dem logischen Auswertungsproblem (Model Checking) zu tun hat. Letztere Beobachtung ist auch ein sinnvoller Ansatz zur Untersuchung der Komplexität dieser praktisch wichtigen Ope...
Prädikatenlogik mit endlichen Modellen
Переглядів 9043 роки тому
Wird Prädikatenlogik einfacher, wenn man statt der bisher vewendeten unendlichen Interpretationen nur noch endliche Interpretationen als Modell zulässt? Macht das überhaupt einen Unterschied für die Semantik? Und was hat das ganze mit Datenbanken zu tun? Diese Fragen sollen in diesem Video beantwortet werden. Wir lernen dabei auch den Satz von Trakhtenbrot kennen. ► Playliste für diesen Videoku...
Die Vollständigkeit der prädikatenlogischen Resolution
Переглядів 5863 роки тому
Endlich schließen wir den Beweis der Vollständigkeit der Resolution ab. Die wenselithce Idee dabei ist es, die Vollständigkeit der aussagenlogischen Resolution auf Herbrandexpansionen in die Ebene der Prädikatenlogik zu "heben": das sogenannte Lifting-Lemma. Aus dem abgeschlossenen Vollständigkeitsbeweis können wir dann noch die Kompaktheit der Prädikatenlogik (erster Stufe) folgern und erste G...
Herbrandexpansionen: Prädikatenlogik auf Aussagenlogik reduzieren
Переглядів 9843 роки тому
Herbrands Idee von "Semantik durch Syntax" lässt sich weiter anwenden, um die Erfüllbarkeit prädikatenlogischer Formeln auf Aussagenlogik zu reduzieren. Außerdem erzähle ich noch die interessante Geschichte hinter der Fotografie Herbrands, welche ich schon im letzten Video gezeigt hatte. ► Playliste für diesen Videokurs: ua-cam.com/play/PLz7XhF-sAU8z4FtL7V9uefCXzW9Z9rk5c.html ► Vorlesungsfolien...
Herbrandmodelle
Переглядів 1,6 тис.3 роки тому
Um die Vollständigkeit der Resolution zu zeigen, wollen wir zunächst von den ziemlich allgemeinen und komplizierten Interpretationen der Prädikatenlogik zu einer einfacheren "syntaktischen" Art von Modellen wecheln: den Herbrandmodellen. Trotz ihrer sehr speziellen Form sind sie in der Lage, die Erfüllbarkeit von Formeln in Skolemform zu charakterisieren. ► Playliste für diesen Videokurs: ua-ca...
Korrektheit der Resolution
Переглядів 4183 роки тому
Der Resolutionssatz stellt die Vollständigkeit und Korrektheit des im letzten Video vorgestellten Algorithmus fest. Ihn zu beweis, wird noch einige Videos in Anspruch nehmen. Die Korrektheit ist dabei der vergleichweise einfache Teil, den wir schon in diesem kurzen Video zeigen können. ► Playliste für diesen Videokurs: ua-cam.com/play/PLz7XhF-sAU8z4FtL7V9uefCXzW9Z9rk5c.html ► Vorlesungsfolien z...
Der Resolutionsalgorithmus
Переглядів 1,5 тис.3 роки тому
Wir schauen uns an, wie Resolution in der Prädikatenlogik funktioniert. Dazu bespreche ich kurz die Unifikation von Atomen und erkläre dann die Resolutionsregel. An einem Beispiel sehen wir, wieso man während der Resolution Varianten bilden muss. ► Playliste für diesen Videokurs: ua-cam.com/play/PLz7XhF-sAU8z4FtL7V9uefCXzW9Z9rk5c.html ► Vorlesungsfolien zum Download: iccl.inf.tu-dresden.de/web/...
Der Unifikationsalgorithmus
Переглядів 1,4 тис.3 роки тому
Zum Lösen von Unifikationsproblemen gibt es einen einfachen Algorithmus, den wir in diesem Video kennenlernen. Wir beweisen außerdem, dass der Algorithmus wie gewünscht funktioniert und zeigen dadurch nebenbei, dass jedes lösbare Unifikationsproblem auch einen allgemeinsten Unifikator hat. ► Playliste für diesen Videokurs: ua-cam.com/play/PLz7XhF-sAU8z4FtL7V9uefCXzW9Z9rk5c.html ► Vorlesungsfoli...
Substitutionen und Unifikation
Переглядів 1,4 тис.3 роки тому
Die wichtigste Neuigkeit beim prädikatenlogischen Schließen im Vergleich zur Aussagenlogik sind die neu hinzugekommenen Terme (aus Variablen, Konstanten und Funktionen). Um mit ihnen logische Schlüsse zu ziehen, müssen wir manchmal Variablen ersetzen (substituieren) damit Terme und letztlich Atome gleich gemacht (unifiziert) werden. Die Grundlagen dazu erklärt dieses Video. ► Playliste für dies...
Die Klauselform in der Prädikatenlogik
Переглядів 1,1 тис.3 роки тому
Im letzten Schritt unserer syntaktischen Vorbereitung auf den Resolutionsalgorithmus wandeln wir die Formel in konjunktive Normalform (KNF) um. Diese kann man dann vereinfacht als Klauselform schreiben. ► Playliste für diesen Videokurs: ua-cam.com/play/PLz7XhF-sAU8z4FtL7V9uefCXzW9Z9rk5c.html ► Vorlesungsfolien zum Download: iccl.inf.tu-dresden.de/web/TheoLog2021 (17. Vorlesung) ► Aktuelle und f...
Existenzquantoren entfernen mit Skolemfunktionen
Переглядів 9443 роки тому
Existenzquantoren lassen sich mithilfe von Funktionen ausdrücken. Diese sogenannte Skolemisierung (nach Thoralf Skolem, 1920) ist ein wichtiger Vorbereitungsschritt für den Resolutionsalgorithmus. Dazu führen wir noch kurz Funktionssymbole in die Prädikatenlogik ein und besprechen, inwiefern sich dadurch (nicht) die Ausdrucksstärke erhöht. ► Playliste für diesen Videokurs: ua-cam.com/play/PLz7X...
Die Pränexform
Переглядів 1,3 тис.3 роки тому
Die Pränexform
Die Negationsnormalform in der Prädikatenlogik
Переглядів 1 тис.3 роки тому
Die Negationsnormalform in der Prädikatenlogik
Prädikatenlogisches Schließen ist semi-entscheidbar
Переглядів 3053 роки тому
Prädikatenlogisches Schließen ist semi-entscheidbar
Prädikatenlogisches Schließen ist unentscheidbar
Переглядів 4713 роки тому
Prädikatenlogisches Schließen ist unentscheidbar
Logisch Schließen mit Gleichheit (Teil 2)
Переглядів 4703 роки тому
Logisch Schließen mit Gleichheit (Teil 2)
Logisch Schließen mit Gleichheit
Переглядів 6163 роки тому
Logisch Schließen mit Gleichheit
Ausagenlogische Gesetze in der Prädikatenlogik
Переглядів 6283 роки тому
Ausagenlogische Gesetze in der Prädikatenlogik
Logische Grundbegriffe verstehen mit ein bisschen Modelltheorie
Переглядів 1,2 тис.3 роки тому
Logische Grundbegriffe verstehen mit ein bisschen Modelltheorie
Prädikatenlogik: Semantik
Переглядів 1,5 тис.3 роки тому
Prädikatenlogik: Semantik
Prädikatenlogik: Syntax
Переглядів 1,6 тис.3 роки тому
Prädikatenlogik: Syntax
Einführung in die Prädikatenlogik
Переглядів 3,3 тис.3 роки тому
Einführung in die Prädikatenlogik
Komplexitätstheorie: Ausblick (und Komplexitäten einiger Spiele)
Переглядів 2743 роки тому
Komplexitätstheorie: Ausblick (und Komplexitäten einiger Spiele)
PSpace-Vollständigkeit 2: Das Spiel Geography
Переглядів 2863 роки тому
PSpace-Vollständigkeit 2: Das Spiel Geography
PSpace-Vollständigkeit 1: TrueQBF und Savitchs Middle-First Suche
Переглядів 3303 роки тому
PSpace-Vollständigkeit 1: TrueQBF und Savitchs Middle-First Suche
PSpace: Schwerer als NP (aber leichter als Schach)
Переглядів 4263 роки тому
PSpace: Schwerer als NP (aber leichter als Schach)

КОМЕНТАРІ

  • @cs_peter_lorenz
    @cs_peter_lorenz 7 днів тому

    Warum genau 2^Q? Warum nicht 3^Q oder 4^Q.

  • @lunte0198
    @lunte0198 18 днів тому

    Was ist bei 3:50 mit "Siehe Vorlesung 2" gemeint? Im zweiten Video der "Automaten und Sprachen" Playlist kommt das gar nicht vor.

  • @abdelrahmanashraf2992
    @abdelrahmanashraf2992 20 днів тому

    Ihre Videos sind toll! Obwohl ich nicht an der TU Dresden studiere, setze ich mich mit dieser Vorlesung auseinander. Ich wünschte, die Lehre an meiner Universität wäre so gut wie die Ihre...

  • @senae.
    @senae. 4 місяці тому

    Dankeschön, sehr hilfreich

  • @Roseroselovely
    @Roseroselovely 5 місяців тому

    super erklärt. vielen Dank. hat mir bei der Klausurvorbereitung enorm geholfen

  • @tangerinegames4515
    @tangerinegames4515 5 місяців тому

    Können Sie Ratschläge dazu geben, wie man bei Reduktionsbeweisen vorgeht zuerst?

  • @Ubilyat
    @Ubilyat 6 місяців тому

    bitte machen sie eine einfache pruefung

  • @aramaljanadi1295
    @aramaljanadi1295 7 місяців тому

    Ich küsse dein kopf

  • @Tagesschatz
    @Tagesschatz 8 місяців тому

    Sie sind zwar nicht mein Professor, aber ich verstehe durch Sie die Sachen sehr gut und besser als durch meinen Professor. Dennoch würde ich Sie gerne fragen, ob solche Beweise auch in Klausuren geführt werden müssen?

  • @ostihpem
    @ostihpem 8 місяців тому

    In Ebbinghaus (Einführung in die math. Logik, 6. Aufl., S. 34) lese ich folgende Definition: Φ ⊨ ϕ :gdw. jede Interpretation, die Modell von Φ ist, ist auch Modell von ϕ. Das kann man doch umformen: Φ ⊨ ϕ :gdw. jedes Modell von Φ ist auch Modell von ϕ. Richtig? Dann muss aber auch gelten, dass ⊨ ϕ :gdw. jedes Modell ist auch Modell von ϕ. Richtig?

  • @kuzco7061
    @kuzco7061 10 місяців тому

    Danke für diese gesamte Videoreihe!!

  • @samankheder2753
    @samankheder2753 11 місяців тому

    danke wie immer für deine tolle erklärungen prof. markus ! Du hilfst mir immer wieder! :)

  • @patrick2092
    @patrick2092 Рік тому

    Vielen Dank für das Video!

  • @csa1999
    @csa1999 Рік тому

    Thumb up fuer die ganze Playlist und Prof Markus!!! Thumb down fuer das Kommentar fuer Horst Muller. Ich fuer meinen Teil bin "Hobby Mathematiker" und schaue mir die Videos freiwillig an. Ich schätze es sehr, dass ich vor meinem smartTV auf der Coach sitzen kann, mit meinem Kaffee in der Hand und die Videos zurück spielen kann, falls ich etwas nicht verstehe. Und das ganze noch gratis, ohne nach Dresden fahren zu muessen, oder Studiengebuehren zahlen zu muessen. (auch gleich gut fuers Klima) Herrn Muller kann ich nur empfehlen sich doch andere Sachen anzuschauen, wenn er an Logik nicht interessiert ist. Und einfach nicht darüber nachzudenken, dass alle Katzen Videos auf UA-cam nur moeglich sind weil es Leute gibt, die schon vor hundert(en) Jahren rein zum Spass über solche Ding nachgedacht haben, wo das Ganze wirklich noch 100% theoretisch war. Herrn Kroetsch, kann ich nur bitten vielleicht auch die anderen Vorlesungen hochzuladen. Ich zumindest wuerde es sehr zu schätzen wissen.

  • @aramaljanadi1295
    @aramaljanadi1295 Рік тому

    Sie sind ein Ehrenmann

  • @csa1999
    @csa1999 Рік тому

    126 + 12 + 7 + 5 +1 = 151 Bei einer Befragung von 152 Experten? Bin jetzt gerade mit der Playlist fertig geworden. War super interessant! Danke

  • @emin6626
    @emin6626 Рік тому

    Vielen Dank! Sehr hilfreich.

  • @reeson
    @reeson Рік тому

    Es macht wirklich einfach Spaß ihnen Zuzuschauen, vielen Dank!

  • @kuzco7061
    @kuzco7061 Рік тому

    Ihr Video hat sogar Brasilien erreicht! Vielen Dank für dieses wunderbare Inhalt!

  • @kuzco7061
    @kuzco7061 Рік тому

    17:00 - Lösungsvorschlag: Bei Kontextsensitiven Sprachen ist die Ableitung oft von den Sachen, die schon abgeleitet wurden abhängig. Bei einer Linksableitung könnte man zuerst zu einer bestimmten Produktionsregel gelangen, die eventuell bei einer Rechtsableitung erst später käme und dabei eventuell eine verschieden Produktionsregel triggert.

    • @kuzco7061
      @kuzco7061 Рік тому

      Habe jetzt gemerkt dass Sie Sekunden danach die Erklärung geben XD

  • @kuzco7061
    @kuzco7061 Рік тому

    Habe riesiges Lerngefühl bei diesen Videos! Man versteht was passiert und man kann es danach auch selbst erklären. Wünschte alle Unis hätten ein*e Prof so wie Sie.

  • @kuzco7061
    @kuzco7061 Рік тому

    Vielen Dank für die ausführliche Erklärung! Auf UA-cam findet man so viele Videos über dieses Thema aber keins ist so methodisch und aufklärend wie Ihres.

  • @kuzco7061
    @kuzco7061 Рік тому

    Vielen Dank für dieses Video. Habe endlich gut verstehen können was die Klasse NP ist und auch woher die Frage NP=CO-NP kommt. Werde es jetzt auf jeden Fall richtig in meiner Klausur antworten können. Tolle Videos!

  • @enamsolaimani414
    @enamsolaimani414 Рік тому

    Sehr gutes Video danke fürs erklären!

  • @wonderland8642
    @wonderland8642 Рік тому

    <3

  • @0x90meansnop8
    @0x90meansnop8 Рік тому

    Sie sind der absolute Wahnsinn, dankeschön :D

  • @lukasnie1500
    @lukasnie1500 Рік тому

    Super Video

  • @LarsL-qy7pj
    @LarsL-qy7pj Рік тому

    Wirklich gut erklärendes video, und auch sehr toll, dass es den kram über git gibt. In Kiel macht man momentan parallel Prolog, und die Technik am Ende um Funktionen über Prädikate zu implementieren hat in meinem Gehirn eine tolle Brücke dazu geschaffen. Danke :)

  • @KnochenMarkSaege
    @KnochenMarkSaege Рік тому

    Vielen Dank für dieses großartige Video, es hat mir wirklich sehr geholfen!

  • @KingStarAlex
    @KingStarAlex Рік тому

    Dank Ihnen schaffe ich die Prüfung an meiner Uni. Vielen Dank!

  • @aalinavalentina
    @aalinavalentina 2 роки тому

    Hallo Herr Prof. Markus, Ich habe eine Bitte könnten sie das Vorgehen erklären wie man von einer KF-Sprache z.b. a*n x b*n *c*n+m zu einem Kellerautomaten kommt? Vielen Dank.

  • @bioroxx
    @bioroxx 2 роки тому

    Ihr Kanal ist goldwert!

  • @linusziegler7086
    @linusziegler7086 2 роки тому

    Sehr gutes Video :)

  • @ligonapProduktion
    @ligonapProduktion 2 роки тому

    Bzgl. Zeitmaschine: Die Paradoxie entsteht nur, wenn man annimmt, dass es nur eine Zeitlinie gibt. Nimmt man aber an, dass es mehrere Zeitlinien parallel gibt, kommt es nie zu einem Paradox. Darüber hinaus existiert die Zeit nur in unserer Realität. Interessant wird es, wenn man annimmt, dass alles was geschehen ist, gerade geschieht oder noch geschehen wird, zur selben Zeit (jetzt) geschieht, nur eben verschoben. Vergleichbar mit einer Papierrolle, bei der die aufgewickelte Papierbahn die Zeit darstellt und alles was geschieht gleichzeitig entlang des Radius geschieht.

  • @ligonapProduktion
    @ligonapProduktion 2 роки тому

    Ich finde, didaktisch sehr gut erklärt. Von mir ein Daumen rauf. 👍

  • @andrabotean
    @andrabotean 2 роки тому

    Hallo, bin ich im Fach "Theoretische Informatik" stecken geblieben. Ich bräuchte Hilfe bei DEAs/NEAs/Kellerautomaten und Turingmaschinen d.h. jemand, der Coach ist oder Nachhilfe im Bereich gibt? (Die Theorie habe ich viele Male durchgearbeitet, brauche aber Übungen und jemanden zur Seite, um zu sehen was ich falsche mache). An wen könnte ich mich da am besten wenden?

  • @horstmuller7512
    @horstmuller7512 2 роки тому

    Gelingt es dir denn wenigstens schon, Logiken niederer Ordnung in der Praxis anzuwenden? Wie schaut es aus beim Rasenmähen (kriegst du da die Kurve?) oder noch simpler: schaffst du es alleine, dir die Schnürsenkel_InInnen zu binden? Jedenfalls scheinen die meisten Kenner von Logiken "höherer Ordnung" in Dummbatzhausen-Süd angesiedelt zu sein, die regelmäßig schon nach wenigen Metern Entfernung nicht den Weg zurück zum eigenen Heim finden.

  • @horstmuller7512
    @horstmuller7512 2 роки тому

    ProgrammiererInInnen? Seufz, waren das noch Zeiten, als es nur Studenten und Studerpel gab, die dann bestens konditioniert von den Unitäten in die Freiheit entlassen wurden, um ohne jedes praktische Wissen ihren Job von der Pike auf zu erlernen (wenn sie nicht schon nach kurzer Zeit wegen erwiesener Dummheit gefeuert wurden). Übrigens scheint eine deiner WasserhähnInInnen zu tropfen - oder was sind das für Hintergrundgeräusche?

  • @xXSkyWalkerXx1
    @xXSkyWalkerXx1 2 роки тому

    Gutes Video! Sollte es (hoffentlich nicht) Thema in meiner morgigen Prüfung sein, hab ich zumindest wenigstens kein kein-Plan. 😅

  • @JO-nn5om
    @JO-nn5om 2 роки тому

    Hallo Herr Krötzsch, vielen Dank für Ihre Videos, die haben mich echt durch die Klausur gerettet!

  • @mayramtokov
    @mayramtokov 2 роки тому

    es ist keineswegs langweilig. Sie haben die besten videos über manche Themen aus Logik auf deutsch. Wenn jemand was besseres findet, linkt es mir in die Kommentare)))

    • @user-jp2kj9ck8y
      @user-jp2kj9ck8y 6 місяців тому

      www.youtube.com/@NLogSpace/videos Ähnlich gut, oftmals ein nicht ganz so theoretischer Ansatz aber auf gleichem Niveau.

  • @lunte0198
    @lunte0198 2 роки тому

    In der Beschreibung heißt es: "Die Antwort wird lauten: zur Turingmaschine.". Aber die wird in dem Video gar nicht erwähnt :p

  • @lunte0198
    @lunte0198 2 роки тому

    Ab 29:00: Warum liegt v |uw| mal vor und wie wird daraus im nächsten Schritt a^(|v|+1)|uw|, insbesondere wo kommt das +1 her?

  • @poshkinshaikho5267
    @poshkinshaikho5267 2 роки тому

    Ich bedanke mich für die ausführliche deutliche Erklärung.

  • @SiphonSoulsX
    @SiphonSoulsX 2 роки тому

    Ah yes UA-cam, let's watch this logic programming (I guess?) video in German, nice recommendation for a non-German speaker

    • @prof.markus6569
      @prof.markus6569 2 роки тому

      True, but isn't it also reassuring that Google does not know you as well as they think they do? Of course, they have to go with what they get from you, e.g., by trying to judge your interests by whether you comment on a video or not ;-) Or maybe they do know you after all - which percentage of UA-cam's audience could identify propositional Horn logic as a form of logic programming? Anyway, at TU Dresden, we also have many free logic-related lectures in English (carefully separated from this German channel); see iccl.inf.tu-dresden.de/web/Courses/en

    • @SiphonSoulsX
      @SiphonSoulsX 2 роки тому

      @@prof.markus6569 I've heard about Horn logic in a propositional logic book from Kazimierz Kuratowski and on some random forum in my endless search for help in bug-fixing, but I'm not a mathematician or a computer scientist, I don't know where UA-cam got this from 😄 Anyways, thanks for the suggestion and good luck in your work!

  • @jaypee6206
    @jaypee6206 3 роки тому

    Why is this in my reccommended?

  • @jan-markuslanger4035
    @jan-markuslanger4035 3 роки тому

    Vielen Dank für die guten Erklärungen.

  • @gulsdznl
    @gulsdznl 3 роки тому

    Danke sehr! Das Video hat mir sehr geholfen :)

  • @codeali3882
    @codeali3882 3 роки тому

    Danke ! Tolles Video

  • @zym123hp
    @zym123hp 3 роки тому

    Respekt für den Regenbogen