Abschnitte dieses Kurses

  • Allgemeines

    Alles einklappen Alles aufklappen

  • Allgemeines

    Das Hauptseminar thematisiert Möglichkeiten und Grenzen des automatisierten Beweisens in  der Prädikatenlogik 1. Stufe mit Identität (FOL). Im Mittelpunkt werden 3 Themenkomplexe stehen: (1) Logische Modellierung: Wie werden nicht-logische Probleme in logische überführt? (2) Unentscheidbarkeitsbeweise: Wo liegen die Grenzen der logischen Entscheidbarkeit? (3) Logische Algorithmisierung: Wie werden logisch entscheidbare Probleme entschieden? Logikkenntnisse und Freude am Arbeiten mit logischen Formeln werden vorausgesetzt. Im Anschluss an das Seminar sollen Sie folgendes können:  (i) Probleme in Form von Entscheidungsproblemen in FOL zu formulieren, (ii) den Unentscheidbarkeitsbeweis für FOL in eigenen Worten wiederzugeben und einer philosophischen Analyse unterziehen, und (iii) Strategien der automatisierten Beweissuche im Rahmen von des Resolutions- und vor allem des Tableauverfahrens kennen.

    Das Seminar wird als online-Kurs durchgeführt und wir werden die sich damit bietenden Möglichkeiten nutzen, das Lehren und Lernen zu individualisieren. Einführungen per Video und Text sowie Lektüre (obligatorisch und weiterführend) stellt dieser Kurs bereit. Zu jedem Thema werden Aufgaben gestellt, die Sie für eine erfolgreiche Teilnahme bearbeiten, mir schicken und gegebenenfalls überarbeiten. Das ist das "Minimalprogramm", das Sie individuell bewältigen und  sich zeitlich flexibel einteilen können. Nur die Termine für die Abgabe müssen Sie einhalten, um das Seminar auch in diesem Semester abzuschließen. Es wird keine obligatorischen Zoom-Meetings geben. Die Gestaltung gemeinsamen Lernens wird vielmehr von Ihnen mitbestimmt. Sie können sich untereinander vernetzen und Lerngruppen bilden (Aufgaben dürfen gemeinsam bearbeitet und abgegeben werden) und Sie können mir Fragen / Anregungen  / Kommentare per e-mail schreiben und bei mir nach individuellen oder gemeinschaftlichen Zoom-Konferenzen anfragen, die wir dann nach Bedarf gestalten. Sie können das Hauptseminar auch nutzen, sich über das Minimalprogramm hinaus in einzelne Themenaspekte tiefer einzuarbeiten und hierbei von mir Hilfestellung erhalten. Ein Hauptseminar sollte immer auch die Möglichkeit bieten, auf eine Masterarbeit vorzubereiten. Wie intensiv Sie sich mit dem Thema (oder Aspekten hiervon) beschäftigen wollen und wieviel Ertrag Sie aus dem Seminar ziehen, wird maßgeblich von Ihnen abhängen. Jede:r hat andere Voraussetzungen und Ziele, die sie / er einbringen kann. Ein hohes Maß an Selbstdisziplin und eine gewisse Zähigkeit beim Lösen von Aufgaben werden dabei vorausgesetzt.

    Lektürehinweise finden Sie zu den einzelnen Themen und Aufgaben, wenn nötig. Drei Empfehlungen vorweg, wenn Sie sich unabhängig von einzelnen Aufgaben einen Überblick verschaffen wollen - Teile dieser Werke / Kurse sind einzelnen Aufgaben zu Grunde gelegt:
    George S. Boolos, John P. Burgess, Richard C. Jeffrey: Computability and Logic, 5th edition, Cambridge University Press, Cambridge.
    (Ein Klassiker, Aufgabe 4 liegt Abschnitt 19.4 (und der Vertiefungsmöglichkeit 21.3) zu Grunde, den Aufgaben zu Thema 2 liegt Abschnitt 3, 4.1, 11.1 zu Grunde).
    Geoff Suttcliffe: Automated Theorem Proving
    (Online Kurs - bietet eine gute Einführung zu Thema 3 auf Basis des Resolutionsverfahrens, Aufgabe 1 und Aufgaben 8 und 9 rekurrieren auf den Kurs)
    Alan Robinson, Andrei Voronkov: Handbook of Automated Reasoning, Vol. 1 und Vol. 2, Elsevier / MIT, Cambridge / MS u.a.
    (Das voluminöse Standardwerk mit vielen Artikeln zu Thema 3, zwei Artikel zum Tablauverfahren werden dem Hauptblock zu Thema 3 zu Grunde liegen)

    Aufgaben 1 und 2 lassen sich direkt angehen, für Aufgaben 3 und 4 sollten Sie an der einführende Zoom-Konferenz teilnehmen und Einführung und logische Modellierung von Goldbachs Vermutung studieren.

  • Logische Modellierung

    Unsere erste Zoom-Konferenz führt Sie anhand der oben angegebenen Folien in die ATP-Welt ein, gibt einen Überblick über Probleme logischer Modellierung und führt anhand der logischen Formalisierung von Goldbachs Vermutung exemplarisch vor, wie mathematische Probleme in logische überführt werden.

    Der Schwierigkeitsgrad der Aufgaben nimmt zu: Für Aufgabe 4 sollten Sie sich an der logischen Modellierung von Goldbachs Vermutung  orientieren und die empfohlene Lektüre lesen. Um die logic engines der TPTP-site verwenden zu können, sollten Sie vorab mit der TPTP-Welt (Abschnitte "Introduction to the TPTP-World" und "Using ATP Systems in the TPTP World") vertraut machen und Aufgabe 1 lösen. Sie brauchen in den Aufgaben nicht Formeln beweisen, sondern generieren (formalisieren). Für Beweise können Sie Theorembeweiser oder Model-Finder verwenden.

    Bitte geben Ihre Lösungen der Aufgaben 1 bis 4 sind bis spätestens 15. Mai, 20 Uhr ab. Im Anschluss werde ich Musterlösungen bereitstellen.

  • Unentscheidbarkeit

    Hier gehen wir andersherum vor: Ein Video mit Musterlösungen gibt es erst im Anschluss an Ihre Lösung. Erarbeiten Sie sich selbstständig den Unentscheidbarkeitsbeweis auf Grundlage der Formalisierung von Turing Maschinen anhand der Darstellung in Boolos et al., Kapitel 3, 4.1 und 11.1. Diese Lektüre stellt den Hintergrund für die Aufgaben dar. Die Formalisierung von Turing Maschinen ist ein weiteres Beispiel der Anwendung der axiomatischen Methoden zum Zwecke der logischen Modellierung von Problemen, in diesem Fall dem Problem, ob eine Turing Maschine auf einen gegebenen input hält. In Aufgabe 5 sollen Sie an einem einfachen Beispiel Fragen über das Verhalten von Turing Maschinen in logische Fragen überführen.  Diese Aufgabe betrifft auch noch Thema 1. Logische Modellierung von Programmcode wird verwendet, um diesen zu verifizieren: Der Code wird formalisiert, um anhand der logischen Schlussfolgerungen zu entscheiden, ob ein Programm auf einen input den intendierten output ausgibt. Im Falle des Unentscheidbarkeitsbeweises kommt die Besonderheit hinzu, dass nicht ein gegebenes Programm formalisiert wird, sondern hypothetisch gefragt wird, ob es möglich ist, dass es ein Programm zur Entscheidung von FOL gibt (= Entscheidungsproblem). Wenn ja, könnte man es formalisieren. Für die negative Lösung des Entscheidungsproblems kommt eine weitere Besonderheit hinzu, dass ein Diagonalfall betrachtet wird, in dem ein hypothetisches Programm zur Entscheidung von FOL mit einer Formalisierung gestartet wird, die die Formalisierung eben dieses Programmes enthält. Aufgabe 6 betrifft die Rekonstruktion des Unentscheidbarkeitsbeweises: hierfür müssen Sie ihn genau verstehen und in eigenen Worten wiedergeben können. Gefragt sind dabei nicht die technischen Details, sondern das Verständnis der Beweisführung. Aufgabe 7 fordert Sie heraus, die Besonderheiten eines Unentscheidbarkeitsbeweises philosophisch zu reflektieren. Wieder nimmt die Schwierigkeit der Aufgaben zu.

    Bitte geben Sie Aufgaben 5 bis 7 bis spätestens 15. Juni, 20 Uhr  ab.

  • Automatisierte Beweissuche

    Während im letzten Abschnitt die Frage der Entscheidbarkeit von FOL von der theoretischen Seite behandelt wurde, wollen wir in diesem Abschnitt diese Frage von der praktischen Seite angehen: Welche Möglichkeiten gibt es, FOL-Formeln algorithmisch zu entscheiden? Dabei wird es nicht um Fragen gehen, die nicht von theoretisch tiefgehender Bedeutung sind, oder die allein die Komplexität der Entscheidungsfindung betreffen. Wir werden deshalb nicht die Frage in den Mittelpunkt stellen, Beweise beweisbarer Formeln oder endliche Modelle erfüllbarer Formeln möglichst schnell und automatisiert zu finden. Die Frage der schnellen Entscheidungsfindung entscheidbarer Formeln werden wir nicht thematisieren, denn sie betrifft nicht die prinzipielle Frage der Grenzen der logischen Entscheidungsfindung: Wenn eine FOL-Formel beweisbar ist, dann wird jeder Theorembeweiser, der diesen Namen verdient, prinzipiell (= gegeben genug Zeit und Speicherplatz) diesen Beweis auch finden; und wenn eine Formel ein endliches Modell hat, dann wird jeder Modelfinder, der diesen Namen verdient, dieses auch prinzipiell finden.

    Interessant und theoretisch tiefgehend wird die Frage, wie FOL-Formeln automatisch entschieden werden können, erst bei der Frage, wie auf automatische Weise bewiesen werden kann, wie nicht-widersprüchliche Formeln, die nur im Unendlichen erfüllbar sind (= infinity axiom sets wie z.B. das aus Aufgabe 3 oder die Formeln zu Goldbachs bzw. Fermats Vermutung), algorithmisch entschieden werden können. Reine Theorembeweiser können in diesem Fall keinen Widerspruchsbeweis finden, und Modelfinder kein endliches Modell. In diesem Fall kann allein die sogenannte "Saturation Method" zu einer Entscheidung gelangen.  Diese Methode sucht im Rahmen eines korrekten und vollständigen Kalküls gezielt nach Widerspruchsbeweisen und versucht auch die "Nicht-Widersprüchlichkeit" durch erschöpfende Anwendung der Kalkülregeln zu entscheiden.

    Die Unentscheidbarkeit von FOL besagt nicht, dass infinity axiom sets nicht algorithmisch entschieden werden könnten. Im Gegenteil, jede endliche Menge an Formeln ist prinzipiell entscheidbar. Die Unentscheibarkeit von FOL besagt nur, dass nicht ein Algorithmus alle (und das sind abzählbar unendlich viele) FOL-Formeln, insbesondere alle (und das sind immer noch abzählbar unendliche viele) infinity axiom sets, entscheiden kann. Wie immer es um den Unentscheidbarkeitsbeweis steht, ist die Frage interessant, die method of saturation von der logischen (nicht meta-logischen) Seite aus auszuloten: Wieweit kann man die automatisierte Beweissuche einschränken, ohne dass Vollständigkeit verloren geht?

    Die Texte und Übungen dieses Abschnittes werden folglich gezielt und schrittweise in das Thema der Entscheidungsfindung von FOL-Formeln mittels der saturation method einführen, so dass Sie am Ende die Frage der Entscheidbarkeit von FOL nicht nur theoretisch mit der Frage der logischen Modellierung von außerlogischen Entscheidungsproblemen (z.B. dem Halte-problem), sondern auch praktisch mit der Frage der Lösbarkeit ganz konkreter logischer Entschreidungsrobleme verbinden können. Hierzu werden wir in 3 Schritten vorgehen:

    1. Allgemeine Voraussetzungen und Umformungen vor Anwendung der saturation method: anti-pränexe clause forms in FOL samt Skolemisierung.

    Aufgabe 8: Umformung in anti-pränexe CNF
    Textgrundlage: Ich habe Ihnen alle nötigen Voraussetzungen zur Lösung von Aufgabe 8 in Clause Forms zusammengestellt.
    Suttcliffe, Clause Normal Form stellt ein anderes Standardverfahren knapp dar, das nicht von anti-pränexen Normalformen Gebrauch macht. Es ist hilfreich, dies zu kennen. Für die Aufgabe sollen Sie aber in anti-pränexe und nicht in pränexe Normalformen umformen.

    2. Reduktion des Entscheidungsproblem auf das Unifikationsproblem: Resolution und Tableaux (Baumkalkül) als Standardkalküle, in deren Rahmen die saturation method zwecks Lösung des Unifikationsproblems definiert wird.

    Aufgabe 9: Beweise im Resolutions- und im Tableauverfahren
    Textgrundlage: Suttcliffes Abschnitt 1st order logic seines Einführungskurs zu ATP gibt eine knappe Übersicht über das Resolutionsverfahren. Eine Einführung in automatisierte Beweissuche im Rahmen von Tableaux gibt:
    - Reiner Hähnle, "Tableaux and Related Methods", in: Alan Robinson und Andrei Voronkov, Handbook of Automated Reasoning, Vol. 1, chapter 3, p. 101 - 178, insbesondere Abschnitt 3 und  Abschnitt 4.2 ("Clause Tableau Proofs") und 4.3 ("Connections"), p.  107-131.
    - Reinhold Letz, Gernot Stenz, "Model Elimination and Connection Tableau Procedures", in: Alan Robinson und Andrei Voronkov, Handbook of Automated Reasoning, Vol. 2, chapter 28, p. 2015-2113. Hier sollten Sie mindestens die Abschnitte 1 und 2 lesen, p. 2015-2025 .
    - Fitting, First Order Logic and Automated Theorem Proving. Insbesondere Kapitel 7 ist für unser Thema einschlägig. Dieses Buch liest sich gut, müssen Sie aber nur konsultieren, wenn Sie Schwierigkeiten haben, die anderen Texte zu verstehen.

     Aufgabe 10: Entscheidbarkeit von CNF mit Klauseln der Länge 1
    Außerdem verlangt  von Ihnen, das Unifikationsproblem und damit das Entscheidungsproblem für ein Fragment von FOL durch Angabe eines konkreten Algorithmus zu lösen, bei der die method of saturation leicht und schnell zu einem Ergebnis gelangt. Diese Aufgabe sollten Sie ohne weitere Literatur allein durch eigenes Nachdenken lösen.

    Aufgabe 11:  Erschöpfende Beweissuche im Tableauverfahren
    Aufgabe 11 thematisiert einfache Beispiele für Beweise der Nicht-Widersprüchlichkeit mittels der method of saturation im Tableauverfahren mit tight connection. In der abschließenden Aufgabe 11.4 sollen Sie sich klar machen, warum die Beweissuche im Tableauverfahren samt den  Optimierungen tight connection, negative clauses, regularity nicht ausreicht, um nicht-widersprüchliche CNFs in jedem Fall zu beweisen.

    3. Loop-Kriterium im Rahmen von Tableau: Entscheidbarkeit von infinity axiom sets.

    Aufgabe 12: Entscheidung von infinity axiom sets und Loop-Kriterium
    Textgrundlage: Lampert, Nakano: A Loop-Criterion for the Proof Search in Clause Tableaux with Tight Connection (Section 1 to 4).
    Diese Aufgabe konfrontiert Sie mit einer Optimierung des Tableauverfahrens mit tight connection, die das Entscheidungsproblem lösen könnte. Sie sollen diese Optimierung verstehen, anwenden und sich mit ihr kritisch auseinandersetzen.

    Bitte geben Sie Ihre Lösungen bis spätestens 30. Juli, 20 Uhr ab.