Moodle.UP

Berechenbarkeit und ihre Grenzen, deterministische und nichtdeterministische Algorithmen, unlösbare Probleme. Komplexität, effiziente Algorithmen, nicht-handhabbare Probleme, Berechenbarkeits- und Komplexitätsklassen, NP-Vollständigkeit und Reduktionen.

In dem Proseminar „Learning meets Algorithm“ werden die Grundlagen des wissenschaftlichen Arbeitens vermittelt. Dies umfasst folgende Lernschritte:

• Recherchieren und Beschaffen wissenschaftlicher Publikationen
• Kennenlernen von unterstützendem Werkzeug für das wissenschaftliche Schreiben
• Erstellen und Validieren von Literaturlisten
• verstehen und zusammenfassen wissenschaftlicher Publikationen
• Erstellen von Gliederungen für wissenschaftliche Ausarbeitungen
• Verfassen und präsentieren einer wissenschaftlichen Ausarbeitung
• wertschätzen und kritisieren unter Peers

Dafür sollen sich die Studierenden mit dem Thema Learning Analytics beschäftigen. Learning Analytics ist ein interdisziplinärer Forschungsbereich, welcher eine Schnittmenge aus Bildungswissenschaften, Informatik und Datenvisualisierung darstellt. Das Ziel ist entstehende und bestehende Daten aus digitalen Lern-/Lehrszenarien zu analysieren und zur Unterstützung des Prozesses den Akteuren zu visualisieren oder die Lernumgebung entsprechend anzupassen. Durch die verschiedenartigen Blickwinkel der Bildungswissenschaften und der Informatik auf das Themengebiet, entstehen spannende interdisziplinäre Diskussionen über u. a. die Einsetzbarkeit von maschinellem Lernen in Lernprozessen, digitale lernunterstützende Umgebungen und Vertrauen in Algorithmen.

Die Studierenden können sich aus vorgestellten Themen ein Bearbeitungsthema auswählen, wozu am Ende des Seminars eine Ausarbeitung angefertigt und in einem Vortrag verteidigt werden soll. Der Schreibprozess wird unterstützt durch Writing Assistance (https://www.uni-potsdam.de/en/zessko/independent-study/writing-assistance) vom Writing Fellow Programm.

Die Veranstaltung gibt eine Einführung in das rechnergestützte Lehren und Lernen aus der Perspektive der Informatik. Es werden zunächst generelle didaktische Szenarien diskutiert und darauf aufbauend Beschreibungsmöglichkeiten, Werkzeuge, Plattformen und Architekturen der IT ausführlich behandelt. Aktuelle E-Learning-Lösungen an der Universität Potsdam und ihre strategische Weiterentwicklung veranschaulichen das Thema. Abschließend wird ein Einblick in verwandte Fragestellungen wie Organisation, Rechte, Geschäftsmodelle u.ä. gegeben.

Vorlesung:
Montag, 10:15 - 11:45 Uhr über Zoom
(Vorlesungsbeginn am 12.04.2021)

Übung:
Mittwoch, 14:00 - 15:30 Uhr über Zoom
(erster Termin am 14.04.2021)

Informatik-Studierende finden Themen der Theoretischen Informatik grundsätzlich interessant, aber korrespondierende Übungsaufgaben -- insbesondere Beweisaufgaben -- stellen immer wieder eine große Herausforderung dar. Der Kurs greift diesen Punkt auf und stellt das mathematische Beweisen in den Mittelpunkt der Auseinandersetzung.

Zum Erlernen der klassischen „Papier&Stift”-Beweise werden wir einen indirekten Weg einschlagen: Zunächst werden wir lernen, mit dem Beweisassistenten Coq Beweise zu führen (Erklärung Beweisassistent s.u.). Später werden wir daran arbeiten, diese Form der Beweise in „Papier&Stift”-Beweise zu übertragen. Schließlich wird auch eingeübt werden, „Papier&Stift”-Beweise direkt zu führen.

Die Inhalte, anhand derer wir die Beweismethodik einstudieren werden, sind die folgenden:
1) Logik
  a) Aussagenlogik
  b) Prädikatenlogik
2) Datenstrukturen
  a) Nicht-rekursive Datenstrukturen (Records)
  b) Listen
  c) Natürliche Zahlen
  d) Binärbäume
Das Ziel allerdings ist hierbei weniger einen konkreten Themenbereich der Mathematik oder Theoretischen Informatik durchzuarbeiten, sondern den Teilnehmerinnen und Teilnehmern des Kurses ein grundlegendes Verständnis mathematischer Beweisformen, formaler Methoden und dem dazugehörigen Handwerkszeug zur Entwicklung und Erstellung dieser zu vermitteln.

Was sind Beweisassistenten?

Computergestützte Systeme zur Durchführung mathematischer Beweise werden seit den 1960ern entwickelt. Man unterscheidet zwischen Systemen, die Beweise erzeugen, sowie solchen, die Menschen beim Erzeugen von Beweisen unterstützen. Letztere werden auch Beweisassistenten oder interaktive Theorembeweiser genannt, ein solches System ist Coq, welches wir im Kurs einsetzen werden.

Bei Beweisassistenten im engeren Sinne des Begriffes kann der Nutzer Schritt für Schritt Wissen aus den Voraussetzungen generieren und das bisherige Ziel durch ein leichter zu zeigendes, aber hinreichendes Ziel ersetzen. Konkret werden Beweise durch eine Auflistung von sogenannten Taktiken innerhalb einer dem Programmieren ähnlichen Entwicklungsumgebung gewonnen, wobei den Taktiken systemintern Inferenzregeln zugrunde liegen. Das System führt die durch die Taktiken vermittelten Inferenzregeln aus. Dabei prüft es jeden Beweisschritt auf seine formale Korrektheit. Dies ist in erster Näherung mit dem Compilereinsatz beim Programmieren vergleichbar.

Beweisassistenten haben gegenüber Stift und Papier verschiedene Vorteile:
-    Sie liefern unmittelbares Feedback auf eine Beweisidee, indem sie genau anzeigen, ob ein Beweisschritt erfolgreich anwendbar ist und welche Schritte noch auszuführen sind, damit ein Beweis vollständig abgeschlossen ist.
-    Studierende können zu Beginn verschiedene Beweisideen ausprobieren, indem sie mit dem jeweiligen System spielen. Das garantiert höhere Flexibilität gegenüber Stift- und Papierbeweisen, in denen man nur sehr schlecht Dinge streichen oder verbessern kann, ohne den Beweis neu aufschreiben zu müssen. Aus dem gleichen Grund sollte ein Beweisassistent auch besser darin unterstützen, mit einem Beweis überhaupt zu beginnen.