Bis zum 6. Juli findet in Nancy eine internationale Forschungsveranstaltung mit Weltexperten für Logik und automatisches Denken statt. Die Gelegenheit, diese Disziplin zwischen Mathematik und Informatik zu erklären.
Es handelt sich um eine internationale wissenschaftliche Veranstaltung, die von INRIA-Wissenschaftlern organisiert wird und bis zum 6. Juli in Nancy stattfindet. Am Institute of Digital Sciences, Management Cognition (IDMC) sind Weltexperten für Logik und automatisches Denken vertreten.
Die Gelegenheit, sich für ein spannendes Forschungsgebiet zu interessieren, das konkrete Anwendungen in unserem täglichen Leben hat. Wir haben die Frage Stephan Merz, INRIA-Forschungsdirektor und Leiter des Veridis-Teams, gestellt.
Es handelt sich um eine Disziplin zwischen Mathematik und Informatik. “Es bietet wesentliche Werkzeuge, um komplexe Probleme methodisch und konsequent zu lösen“, erklärt Stephan Merz.
Automatisiertes Denken ist der Bereich der Informatik, der versucht, Garantien dafür zu geben, was ein System oder Programm tun wird oder was nie. Diese Zusicherung basiert auf mathematischen Beweisen.
Um logische Probleme in der Mathematik, Mathematik oder Geometrie zu lösen, verwenden wir Theoreme und Schlussfolgerungen, also logische Strategien. Beim automatisierten Denken kommen Computer zum Einsatz, die zur Lösung komplexer Probleme dieselben Werkzeuge verwenden.
Logik und automatisches Denken haben unterschiedliche Anwendungen in verschiedenen Bereichen. “Es ist leicht vorstellbar, dass im Bereich der Luftfahrt oder der Eisenbahn eine Zertifizierung erforderlich ist, bevor Software in Betrieb genommen wird. Dabei ist es wichtig, bestimmte Korrektureigenschaften zu gewährleisten, zum Beispiel, dass nie zwei Züge denselben Gleisabschnitt belegen, dass die U-Bahn vor den Brückenbrücken hält oder dass zwei Flugzeuge immer einen Mindestabstand einhalten. Auf der anspruchsvollsten Ebene dieser Zertifizierungen wird empfohlen, diese formalen Beweistechniken zu verwenden, um diese Eigenschaften zu gewährleisten. Wir benötigen diese sehr ausgefeilten und automatisierten Techniken für diese kritischen Systeme“, erklärt der INRIA-Forschungsdirektor.
Die gleichen Techniken werden in Systemen mit hohem finanziellen Einsatz eingesetzt, beispielsweise im Online-Speicher- und -Verarbeitungssystem, der Cloud. Unternehmen müssen die Verfügbarkeit ihrer Dienste gewährleisten, was auch für Bankensysteme von Nutzen ist.
In der Programmierung wird Logik zum Schreiben von Algorithmen und Computerprogrammen verwendet. Automatische Argumentation ermöglicht es, die Gültigkeit von Programmen zu überprüfen. Es könnte als Teil des selbstfahrenden Autos verwendet werden, um Sicherheitssysteme zur Steuerung der Vermeidung zu gewährleisten.
Immer mehr Unternehmen, die Software entwickeln, wenden sich an Spezialisten für formale Methoden, um die ordnungsgemäße Funktion kritischer Computerkomponenten computergestützt zu überprüfen, insbesondere mithilfe automatischer Argumentationstechniken. Der Grund: Jede Anomalie könnte dramatische Folgen haben.
“Einige Experten für automatische Abzüge arbeiten für GAFAM oder für die Raumfahrtagenturen NASA oder ESA“, sagt Stephan Merz.
In diesem Jahr 2024 wurde die Stadt Nancy als Gastgeber dieser internationalen Veranstaltung ausgewählt. Es wird von Wissenschaftlern des Inria-Zentrums und der Universität Lothringen organisiert. Die Forschungsteams der Universität Lothringen und des Inria-Zentrums stehen an der Spitze der wissenschaftlichen Arbeiten in diesem Bereich.
Die Organisation einer solchen Konferenz ist entscheidend dafür, Nancy weiterhin zu einer starken Stellung in den Bereichen formale Methoden, Verifizierung komplexer Systeme und automatisches Denken zu machen.
Bis zum 6. Juli werden am Institute of Digital Sciences, Management Cognition (IDMC) in Nancy Workshops und Konferenzen organisiert.
