Den Hammer härten: Mehr Integration von automatischen und interaktiven Theorembeweisern

• Antragsteller: Professor Tobias Nipkow, Ph.D.
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2012 bis 2016
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 226154341

Interaktive Theorembeweiser (ITPs) werden zunehmend dazu verwendet, die Korrektheit komplexer und sicherheitskritischer Algorithmen und Systeme nachzuweisen. ITPs bauen auf ausdrucksstarken Logiken auf, sind aber sehr zeitaufwendig in der Benutzung. Automatische Theorembeweiser (ATPs) dagegen bauen auf einfachen Logiken auf, die besser automatisierbar sind. Dieser Antrag setzt es sich zum Ziel, ITPs und ATPs besser zu integrieren, um den Automatisierungsgrad von ITPs zu erhöhen und es damit zu ermöglichen, komplexere Theoreme in kürzerer Zeit zu beweisen.Die Basis für unsere praktischen Arbeiten ist der weit verbreitete ITP Isabelle/HOL. Sledgehammer ist ein Teil von Isabelle/HOL. Er realisiert eine Ankopplung der mächtigsten zur Zeit erhältlichen ATPs an Isabelle/HOL um die interaktive Beweiskonstruktion zu unterstützen. Sledgehammer ist seit fünf Jahren verfügbar und ist zu einem essenziellen Werkzeug für Isabelle Benutzer geworden. Es ist die einzige Kopplung zwischen einem ITP und ATPs, die bei Benutzern derart erfolgreich ist. Sledgehammer hat völlig verändert, wie Anfänger Isabelle wahrnehmen.Dieses Projekt wird die folgenden Aspekte der ITP/ATP Kopplung grundlegend erweitern. Im Moment sind Sledgehammer Beweise unverständlich; jetzt wollen wir die maschinellen ATP Beweise in für den Menschen lesbare Beweise transformieren. Im Moment ist Sledgehammer auf die Logik HOL beschränkt.; jetzt wollen wir ihn auf Mengenlehre erweitern, die Grundlage nicht nur aller Mathematik sondern auch von Lamports TLA+, einer Logik und eines Systems zur Software Spezifikation und Verifikation. Im Moment kann Sledgehammer nur schlecht mit Mengen und höherstufigen Konstrukten umgehgen; jetzt wollen wir neue Kodierungen höherstufiger Konstrukte in erststufiger Logik (wie sie von den ATPs unterstützt wird) entwickeln und empirisch bewerten. Im Moment übersetzt Sledgehammer in untypisierte erststufige Logik; jetzt wollen wir die neuesten Erweiterungen der ATPs im Bereich der Typsysteme und eingebauter Theorien integrieren.Wichtige Aspekte unseres Antrags sind die große Anzahl der Isabelle Benutzer, die von unserer Forschung direkt profitieren werden, die exzellente Datenbasis (in der Form großer Beweis-Bibliotheken) für empirische Auswertungen, und unsere enge Zusammenarbeit mit der ATP Community um eine optimale Anpassung von ITP und ATPs zu erreichen.

• DFG-Verfahren: Sachbeihilfen