Johannes C. Schuster

Ich habe vor Kurzem mein Masterstudium der Angewandten Informatik an der Otto-Friedrich-Universität Bamberg mit Schwerpunkt Künstliche Intelligenz abgeschlossen. Meine Masterarbeit wurde von Prof. Dr. Christoph Benzmüller (Lehrstuhl für KI-Systementwicklung) betreut, an dessen Lehrstuhl ich weiterhin arbeite und eine Promotion anstrebe.

Während meines Studiums habe ich mich intensiv mit den theoretischen Grundlagen des maschinellen Lernens und des automatischen Theorembeweisens befasst. Meine Kernkompetenzen liegen in den Bereichen Logik höherer Stufe, mathematische Grundlagen des maschinellen Lernens, natürliche Sprachverarbeitung, funktionale Programmierung und neuro-symbolische KI.

Ein großer Teil meiner aktuellen Arbeit ist Infrastruktur für automatisches Schließen auf der BEAM (Elixir/Erlang): tptp, ein Parser, Linter und Printer für die TPTP-Sprache; AtpClient, ein einheitlicher Zugang zu externen Beweisern; und Shot, der nebenläufige Tableau-Beweiser für Logik höherer Stufe, den ich in meiner Masterarbeit entwickelt habe. Gemeinsam mit Geoff Sutcliffe (University of Miami) überarbeite ich die SZS-Ontologien, den Standard, in dem automatische Beweiser ihren Ergebnisstatus melden; ich habe die Erfolgsontologie in Isabelle/HOL formalisiert, aus der die Hierarchie abgeleitet und gegen die die veröffentlichte Grammatik geprüft wird.

Mein geplantes Promotionsvorhaben, Certified Parallel Tableaux for Higher-Order Logics with Language Model Instantiations, baut auf Shot auf. Es entwickelt einen Free-Variable-Tableaukalkül für die klassische Logik höherer Stufe mit destruktiver Substitution und OR-paralleler Suche über Instanziierungskandidaten und soll dessen Korrektheit und Vollständigkeit bezüglich der Henkin-Semantik mit Auswahl (Choice) nachweisen. Ein Sprachmodell soll innerhalb der Suche Instanziierungen vorschlagen, der Kalkül prüft jeden Vorschlag, und jede Antwort soll mit einem Zertifikat versehen werden, das ein kleiner unabhängiger Verifizierer gegen eine explizite Axiomatisierung der Logik höherer Stufe prüft. Die Übertragung des Kalküls auf die abhängig getypte Logik höherer Stufe ist als Erweiterung vorgesehen.