idw – Informationsdienst Wissenschaft
Nachrichten, Termine, Experten
Nachrichten, Termine, Experten
In der CADE ATP System Competition, der Weltmeisterschaft für automatische Beweiser, besteht die SLH-Division (Sledgehammer-Division) aus Beweisaufgaben, die menschliche Nutzer*innen mit dem interaktiven Beweiser „Isabelle“ beweisen wollen und die in eine für automatische Beweiser geeignete Logik übersetzt wurden. In dieser Division hat der an der DHBW Stuttgart entwickelte Theorembeweiser „E“ den Wettbewerb im Rahmen der FLoC Olympic Games in Haifa (Israel) gewonnen.
Prof. Dr. Stephan Schulz trat mit „E“ in sechs der insgesamt sieben Divisionen an und erzielte neben dem ersten Platz in SLH auch drei zweite Plätze in den Divisionen FOF (klassische Prädikatenlogik erster Stufe, die "Königsdisziplin"), UEQ (unbedingte Gleichheitslogik) und THF (Prädikatenlogik höherer Stufe). Einen dritten Platz gab es in der Division LTB (Beweisaufgaben mit sehr großen Axiomenmengen in verschiedenen Codierungen).
„If all you have is a hammer, every problem looks like a nail – wenn du nur einen Hammer hast, sieht jedes Problem aus wie ein Nagel “ war wohl die Inspiration, die Lawrence Paulson an der Universität Cambridge dazu bewegte, automatische Theorembeweiser als Back-End für den interaktiven Beweiser „Isabelle“ einzusetzen und diesen Ansatz Sledgehammer (=Vorschlaghammer) zu nennen.
Theorembeweiser sind Computerprogramme, mit denen man formal nachweist, dass bestimmte Aussagen zwingend aus einer gegebenen Beschreibung folgern. Beispiele im Kleinen wären z. B. die Beweise, dass ein Computerprogramm immer innerhalb einer bestimmten Zeit reagiert (und etwa die Bremse eines autonomen Fahrzeuges betätigt), oder dass eine Banktransaktion immer entweder vollständig oder gar nicht abgewickelt wird. Im Großen kann inzwischen die funktionale Korrektheit von komplexen Programmen wie z. B. einem Betriebssystemkern nachgewiesen wer-den und es gibt Projekte, in denen große Teile der klassischen Mathematik noch einmal formal nachgebildet werden.
Interaktive Beweiser wie „Isabelle“ unterstützen typischerweise Prädikatenlogik höherer Stufe und damit einen sehr mächtigen Formalismus. Sie verlassen sich aber darauf, dass ein Benutzer bzw. eine Benutzerin den Beweisvorgang steuert und fast alle wichtigen Entscheidungen über anzuwendende Taktiken selbst trifft - z. B. Fallunterscheidung, Induktion oder Beweis durch Widerspruch. Automatische Beweiser dagegen setzen in der Regel auf die Prädikatenlogik erster Stufe, bieten dafür aber hohe Geschwindigkeit, vollständige Kalküle und eine vollautomatische Beweissuche. Sledgehammer, das von Paulson erdachte und inzwischen mit vielen anderen Wissenschaftlern weiterentwickelte Werkzeug, wandelt Teilaufgaben des interaktiven Beweisers automatisch in geeignete Probleme für vollautomatische Beweiser um und entlastet damit die Nutzer*innen solcher Systeme ganz erheblich.
URLs:
- E https://www.eprover.org
- FLoC: https://www.floc2022.org/
- CADE ATP System Competition: https://www.tptp.org/CASC/J11/
- Stephan Schulz: https://www.dhbw-stuttgart.de/~sschulz
Prof. Dr. Stephan Schulz
https://expertenservice.dhbw-stuttgart.de/experteninnen-technik/informatik/steph...
Merkmale dieser Pressemitteilung:
Journalisten, Wirtschaftsvertreter, Wissenschaftler
Informationstechnik, Mathematik
überregional
Forschungs- / Wissenstransfer, Wettbewerbe / Auszeichnungen
Deutsch
Sie können Suchbegriffe mit und, oder und / oder nicht verknüpfen, z. B. Philo nicht logie.
Verknüpfungen können Sie mit Klammern voneinander trennen, z. B. (Philo nicht logie) oder (Psycho und logie).
Zusammenhängende Worte werden als Wortgruppe gesucht, wenn Sie sie in Anführungsstriche setzen, z. B. „Bundesrepublik Deutschland“.
Die Erweiterte Suche können Sie auch nutzen, ohne Suchbegriffe einzugeben. Sie orientiert sich dann an den Kriterien, die Sie ausgewählt haben (z. B. nach dem Land oder dem Sachgebiet).
Haben Sie in einer Kategorie kein Kriterium ausgewählt, wird die gesamte Kategorie durchsucht (z.B. alle Sachgebiete oder alle Länder).
