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...
Criteria of this press release:
Business and commerce, Journalists, Scientists and scholars
Information technology, Mathematics
transregional, national
Contests / awards, Transfer of Science or Research
German
You can combine search terms with and, or and/or not, e.g. Philo not logy.
You can use brackets to separate combinations from each other, e.g. (Philo not logy) or (Psycho and logy).
Coherent groups of words will be located as complete phrases if you put them into quotation marks, e.g. “Federal Republic of Germany”.
You can also use the advanced search without entering search terms. It will then follow the criteria you have selected (e.g. country or subject area).
If you have not selected any criteria in a given category, the entire category will be searched (e.g. all subject areas or all countries).
