3 - Einheit 3/4: „Gastvortrag Prof. Dr. Alexander Stehen – Uni Greifswald: „Einführung in Logik und automatisches Schließen““ [ID:42321]
50 von 964 angezeigt

Also erstmal dann vielen Dank für die Einladung. Ganz kurz zu meiner Person, Axel hat ja schon ein

bisschen was erzählt. Die Frage, was ich eigentlich genauso bin, ob jetzt Mathematiker,

Informatiker, ist gar nicht einfach zu beantworten. Ich habe beide studiert. In Berlin habe ich sowohl

Mathe als auch Informatik studiert, aber dann nur in Informatik den Master gemacht und dann auch im

Anschluss in Berlin an der Freien Universität promoviert zu einem Thema der KI, zur symbolischen KI.

Hier im Englischen wird man es eher als Computational Logic beschreiben. Computationale

Logik, also Logik auf der Maschine, auf dem PC. Ich habe hier eine Dissertation geschrieben, wo ich

unter anderem ein System entwickelt habe, das eben autonom, wenn man so möchte, auf dem Rechner

versucht logische Schlussfolgerungen zu ziehen. Was das genau bedeutet, werden wir gleich im Vortrag

so ein bisschen sehen. Danach war ich seit Mitte 2018 Postdoc in Luxemburg und habe mich da dann

auch verstärkt mit den Anwendungen von Logik beschäftigt, insbesondere mit Anwendungen im

normativen Kontext. Das heißt also hier auch genau die Richtung, warum die Kooperation hier quasi

sehr fruchtvoll ist. Logiken für Sollensnormen, für Dürfensnormen und wie man die auf den Rechnern

bringen kann, um eben auch auf dem Rechner automatisierte Schlussfolgerungen über solche

Normen ziehen zu können. Seit 2022 bin ich jetzt ganz frisch, also seit vier oder fünf Monaten,

wir haben schon Mai, also seit ungefähr fünf Monaten, Juno-Professor für Informatik an Uni

Galswald. Genau und war auch vorher noch mal ein bisschen in der Wirtschaft unterwegs, relativ

kurz als freiberuflicher Software-Entwickler. Mich zieht es aber eher in die akademische

Richtung, bin aber trotzdem noch am Programme entwickeln. Was ich üblicherweise tue, womit ich

meine Zeit quasi verbringe, ist, zumindest inhaltlich gesehen, dass ich interessiert bin

an der Theorie von logischen Schlussfolgerungen auf dem Rechner. Das nennt sich hier Automated Reasoning,

also das automatisierte Schlussfolgern auf dem Rechner. Da geht es insbesondere darum,

wie wir das mechanisiert machen können. Das ist quasi genau der Aspekt hier von Proof Calculie,

also von Beweis-Kalkülen und natürlich auch, wie ich die entsprechend effizient auf dem Rechner

implementieren kann. Die praktischen Aspekte von Automated Reasoning sind insbesondere,

wie kann ich tatsächlich die mathematische Theorie auf den Rechner bringen, so dass ich

tatsächlich Software habe, die ich am Ende ausführen kann, die für mich die logische

Schlussfolgerung auch durchführt. Und natürlich, die Software ist nichts so richtig wert aus meiner

Sicht, wenn man nichts Sinnvolles mit ihr tun kann. Darum bin ich insbesondere auch interessiert an

Anwendungen von Automated Reasoning, also von automatisierten Schlussfolgern, insbesondere

in den letzten Jahren im legalen, also legal, also juristischen, im normativen Kontext. Hier

sind so die Schlagworte die ontische Logiken, also Logiken über Normen. Aber auch in der

Argumentation habe ich gearbeitet und das sind jetzt so die Schwerpunkte, mit denen ich auch

in den nächsten Jahren beschäftigen werde. Und was man auf jeden Fall kriegen kann, wenn man sich

mit automatischen Beweissystemen, die werden auch automatische Theoriebeweiser genannt,

beschäftigt und die tatsächlich implementiert, dann kann man zu der jährlichen Meisterschaft

gehen. Natürlich, es gibt für alles mögliche Weltmeisterschaften, also auch für logische

Schlussfolgern, das ist tatsächlich kein Scherz, das sind die CASC-Weltmeisterschaften,

CATE-ATP System Competition. Hier werden tatsächlich jedes Jahr bestimmt mindestens 15-20

Theoriebeweiser hingeschickt als Software und die werden dann in einer Meisterschaft antreten und

jedes Jahr versuchen so viele Probleme wie möglich zu beweisen. Das bedeutet wirklich,

zeigen zu können, formal, dass aus gewissen Annahmen eben gewisse Schlussfolgerungen so sein

müssen, also quasi mathematische Beweise finden und wenn man das gewinnt, so wie wir im Jahr 2019,

dann kriegt man so ein Plastikpokal, der sicherlich in Anschaffungskosten bei zwei Dollar lag oder so,

aber komischerweise bringen es die zwei Dollar-Pokale weit aus mehr als ein Preisgeld von 100 Dollar.

Also diese Pokale will jeder in der Community haben und wenn Sie sich spontan entscheiden

sollten, dass Sie auch so ein Pokal haben wollten, schreiben Sie mich gerne an, da gibt es noch viel

zu tun. Also genau, da ist also erstmal vorweg zu dem, womit ich mich beschäftige. Was haben wir

nun Heuke vor? Das ist der Plan für Heuke. Ich hätte eine Frage. Ja, unbedingt. Gibt es eine Folie,

auf die wir uns dann für das Lernen beziehen können? Genau, ich werde jetzt gleich einen

Zugänglich über

Offener Zugang

Dauer

01:37:43 Min

Aufnahmedatum

2022-05-24

Hochgeladen am

2022-05-24 19:46:06

Sprache

de-DE

Einbetten
Wordpress FAU Plugin
iFrame
Teilen