Können Computer denken? Automatisches Beweisen und künstliche Intelligenz
Arbeitsgruppe 4, Akademie Leysin, Schweiz, Studienstiftung des deutschen Volkes
12. August 2018 – 25. August 2018
Beschreibung: (siehe
Jahresprogramm 2018, S. 19)
Während die eigenständig und kreativ denkende Maschine noch ein ferner Zukunftsgedanke
ist, wurden im Bereich der künstlichen Intelligenz in den letzten Jahren diverse spannende
Durchbrüche erzielt und vielversprechende Entwicklungen angestoßen. Die Methoden der
künstlichen Intelligenz genügen bereits heute, um dem Menschen viele Aufgaben abzunehmen,
die durch ein hohes Maß an Routine charakterisiert sind. Man denke beispielsweise
an Internetsuchmaschinen, Routenplaner, Schachcomputer, Übersetzungsprogramme oder
Staubsaugroboter. Immer mehr menschliche Betätigungsfelder im Alltag und in der Wissenschaft
werden so im Zuge der fortschreitenden Digitalisierung automatisiert – aber gilt dies
auch für die Mathematik?
In unserer Arbeitsgruppe möchten wir uns Schritt für Schritt dem aktuellen Forschungsstand
in der Anwendung künstlicher Intelligenz auf die formale Mathematik nähern. Wir wollen
untersuchen, inwieweit sich das Verstehen, Beweisen und Entdecken mathematischer
Zusammenhänge automatisieren lassen. Es wird Gelegenheit sowohl zum theoretischen
Durchdringen der relevanten Methoden und Konzepte als auch zur praktischen Umsetzung
von Algorithmen und Programmen geben. Es werden keine wesentlichen Vorkenntnisse
vorausgesetzt.
Zielgruppe: Studierende der Natur- und Ingenieurwissenschaften sowie der Mathematik und motivierte Studierende anderer Fächer bis zum 4. Semester.
Dozierende:
Material
Vorbereitungshinweise
Prädikatenlogik erster Stufe
Themenblock I – Mathematische Logik
Tutorial Isabelle
Isabelle: FOL – Lösungen
Formalising propositional logic
Prolog: Vier-Farben-Satz Australien
Prolog: Propositional Logic
OCaml: Einführung und Propositional Logic
Formalizing first-order logic
OCaml-Code aus Harrisons Buch
Modelltheoretische Grundlagen – Syntax und Semantik
Mechanizing first-order logic: Unification
Maschinelles Lernen
Python/Jupyter: Lineare Regression –
(html)
Python/Jupyter: Logistische Regression –
(html)
Python/Jupyter: Neuronale Netze –
(html)
Themen für die Projektphase
Projektergebnisse
Haskell: Entscheidungsalgorithmus für reelle Zahlen –
Ausgabe (Thema 2)
NIP, O-Minimalität und neuronale Netze (Thema 5)
Letzte Änderung / Last update:
