Der interaktive Theorembeweiser Lean gewann in den letzten Jahren an Bedeutung. Ein prominentes Beispiel dafür ist die Verwendung von Lean von der mathematischen Gemeinschaft im Projekt zur Formalisierung der Mathematik in Mathlib. Ein attraktives Merkmal von Lean ist der kleine vertrauenswürdige Kern. Die Aufgabe des Kerns ist es, zu überprüfen, ob die formulierten Theoreme tatsächlich solche sind. Der Kern von Lean selbst ist nicht formal verifiziert, aber seine kleine Größe und seine klare Aufgabenstellung erzielen ein hohes Maß an Vertrauen in seine Korrektheit. Beweise in Lean zu schreiben kann sich als recht mühsam erweisen, weshalb es ein großes Anliegen ist, das Schreiben von Beweisen zu vereinfachen. Eine Methode, mit der es einfacher wird, Beweise zu schreiben, sind Automatisierungswerkzeuge, die für einfachere Theoreme vollautomatisch einen Beweis liefern können. Die „Thousands of Problems for Theorem Provers“ (TPTP, deutsch: Tausende Probleme für Theorembeweiser) Problembibliothek ist eine große Sammlung an Problemformulierungen, die in einem Format geschrieben ist, das von gängigen automatischen Theorembeweisern als Eingabe akzeptiert wird. Die Probleme der Bibliothek stammen aus verschiedenen Domänen und sind in unterschiedlichen Logiken und Theorien formuliert. Diese Bibliothek dient als Maßstab zur Evaluierung von automatischen Theorembeweisern. In dieser Arbeit stellen wir eine Übersetzung von Instanzen der TPTP-Problembibliothek nach Lean vor. Diese Übersetzung ist in zwei Lean Bibliotheken implementiert, die es ermöglicht, Instanzen die im TPTP-Format geschrieben wurden als Ausdrücke in Lean zu importieren. Durch diese Übersetzung steht die TPTP-Problembibliothek als Maßstab für Automatisierungswerkzeuge in Lean zur Verfügung. Wir nutzen diese Übersetzung um existierende Automatisierungswerkzeuge zu evaluieren. Wir analysieren die Leistungsfähigkeit unserer Werkzeuge indem wir sie mit der von Lean auf äquivalenten Eingaben vergleichen.
de
The interactive theorem prover (ITP) Lean has gained much popularity in recent years. A prominent example for the adoption of Lean is given by the mathematical community’s formalization effort in Mathlib. One of Lean’s attractive features is that of a small trusted kernel. The kernel’s job is to check that the proofs of stated theorems are in fact correct. Lean’s kernel itself is not formally verified but due to its relatively small size and clear-cut goal is assumed to provide a high assurance of correctness. Writing proofs in Lean can be quite labor-intensive and therefore there is considerable effort expended in making it easier for users to write proofs in Lean. One way in which users are supported is in the forms of automation tools that are able to construct reasonably simple proofs automatically. The Thousands of Problems for Theorem Provers (TPTP) problem library is a large repository of problem statements in a format that is commonly used as input for first- and higher-order automated theorem provers (ATPs). The problems come from a broad range of domains and are expressed in different logics and theories. This provides an extensive set of benchmarks to evaluate ATPs. In this thesis we provide a translation that brings instances of the TPTP problem library to Lean. This translation is implemented in the form of two Lean libraries that allow users to import instances written in the TPTP format as Lean expressions. With this translation the TPTP problem library becomes available as a benchmark set for automation tools inside Lean. We use this translation to evaluate some of the existing automation tools in Lean. We analyze the performance of our tools by comparing it with that of the Lean compiler on equivalent instances.
en
Additional information:
Arbeit an der Bibliothek noch nicht eingelangt - Daten nicht geprüft
