Logisches Schlussfolgern durch symbolische KI

Automatisches Schlussfolgern. Prof. Alexander Steen forscht auf dem Gebiet der symbolischen künstlichen Intelligenz. Insbesondere beschäftigt er sich mit dem automatischen Schlussfolgern, bei dem expressive Logiken verwendet werden, um allgemeine Gesetzmäßigkeiten der Welt zu beschreiben. Durch diese Form der Beschreibung kann computergestützt entschieden werden, ob eine Aussage wahr oder falsch ist. Diese Systeme werden bereits in der mathematischen Beweisführung oder der Software-Verifikation eingesetzt. Diese Systeme können auch bestehende Ansätze des maschinellen Lernens ergänzen, um den systematischen Bias bzw. Verzerrungen in der Datenerhebung zu reduzieren.

Beweisstandardisierung. Außerdem setzt sich Prof. Steen mit der Standardisierung von logischen Beweisen auseinander. Dadurch werden die logischen Beschreibungen portabler und können von unterschiedlichen Tools verarbeitet werden, ohne erst neu angepasst werden zu müssen. Die Arbeit von Prof. Steen findet nicht nur in mathematischen Beweisführung Verwendung, sondern ist sowohl in der der Metaphysik, in der Philosophie als auch in der Rechtswissenschaft anwendbar.  So können Normen, Gesetze und Glauben logisch modelliert und Folgerungen aus ihnen geschlossen werden.  Des Weiteren stellt die Nachvollziehbarkeit dieser Schlussfolgerungen einen Aspekt da, der in diesem Bereich einen hohen Wert einnimmt. 

Kompetenzen im Bereich der künstlichen Intelligenz und Data Science

  • Symbolische Künstliche Intelligenz
  • Automatisches und interaktives Theorembeweisen, Logikautomatisierung
  • Expressive und nichtklassiche Logiken
  • Systemimplementierung

Jun.-Prof. Dr. Alexander Steen

Informatik, Universität Greifswald

Ausgewählte Projekte

Leo-III – Effective Automation for Higher-Order Logic

Das open-source System Leo-III ist ein automatischer Theorembeweiser für ausdrucksstarke höherstufige Logiken. Mithilfe eines solchen Systems können mathematische Fragestellungen modelliert und anschließend bearbeitet werden – sodass in vielen Fällen die mathematischen Behauptungen vom System autonom bewiesen oder widerlegt werden. Allerdings ist Leo-III auch Vorreitersystem für die Automatisierung von nichtklassischen Logiken, die für die Modellierung von Szenarien aus der theoretischen Philosophie, der Künstlichen Intelligenz oder den Rechtswissenschaften genutzt werden kann.
Leo-III und zugehörige Projekte sind frei auf GitHub unter https://github.com/leoprover/ verfügbar.


AuReLeE – Automated Reasoning with Legal Entities

Das Ziel des Projekts Automated Reasoning with Legal Entities (AuReLeE) ist es, effektive und allgemeine Mittel für die Automatisierung von normativen Argumentationsprozessen auf der Basis von juristischen Wissensbasen bereitzustellen. Dabei sollen effiziente Entscheidungsprozeduren mit einem flexiblen Ansatz zum Import und zur Wiederverwendung bestehender Wissensbasen kombiniert werden, um diese als zugrundeliegende Kontexte für die normativen Argumentationsaufgaben zu nutzen. AuReLeE soll somit die volle Nutzung des Potenzials vorhandener juristischer Wissensbasen für die Compliance-Prüfung ermöglichen.
https://www.alexandersteen.de/projects/aurelee/


National Research Data Infrastructure for and with Computer Science (NFDIxCS)

Prof. Steen ist Teilnehmer des NFDIxCS-Konsortiums. Das Hauptziel des Konsortiums NFDIxCS ist die Identifizierung, Definition und Bereitstellung von Diensten zur Speicherung komplexer domänenspezifischer Datenobjekte aus der spezifischen Vielfalt der Teilgebiete der Informatik und die durchgängige Umsetzung der FAIR-Prinzipien. Dies beinhaltet die Erstellung von wiederverwendbaren Datenobjekten, die spezifisch für die verschiedenen Arten von Informatik-Daten sind und nicht nur diese Daten zusammen mit den zugehörigen Metadaten, sondern auch die zugehörigen Software-, Kontext- und Ausführungsinformationen in einer standardisierten Weise enthalten. Diese Datenobjekte können von beliebiger Größe, Struktur und Qualität sein.
https://nfdixcs.org/