Go to page
 

Bibliographic Metadata

Title
Learning Proof Search in Proof Assistants
Additional Titles
Learning Proof Search in Proof Assistants
AuthorFärber, Michael
Thesis advisorKaliszyk, Cezary
Published2018
Institutional NoteInnsbruck, Univ., Diss., 2018
Date of SubmissionJuly 2018
LanguageEnglish
Document typeDissertation (PhD)
Keywords (DE)Logik / automatische Beweissuche / Theorembeweiser / Beweisassistent / maschinelles Lernen / Prämissenselektion / Beweisübersetzung
Keywords (EN)logic / automatic proof search / theorem prover / proof assistant / machine learning / premise selection / internal guidance / proof translation
URNurn:nbn:at:at-ubi:1-30047 Persistent Identifier (URN)
Restriction-Information
 The work is publicly available
Files
Learning Proof Search in Proof Assistants [1 mb]
Links
Reference
Classification
Abstract (German)

Beweisassistenten sind Programme zur Verifikation der Korrektheit von formellen Beweisen. Sie können das Vertrauen in Resultate aus Bereichen wie Mathematik, Informatik, Physik und Philosophie erhöhen. Allerdings erfordert es hohen Arbeitsaufwand und Expertise, um Beweise zu schreiben, die von Beweisassistenten akzeptiert werden. In dieser Doktorarbeit verbessern wir die Beweisautomatisierung in Beweisassistenten.

Automatische Theorembeweiser sind Programme, die automatisch nach Beweisen suchen. Unser Ziel ist es, Beweise in Beweisassistenten mithilfe von automatischen Theorembeweisern zu finden. Allerdings ist dies nicht direkt möglich, wenn sich die Logik eines automatischen Theorembeweisers und die Logik eines Beweisassistenten unterscheiden.

In diesem Fall erfordert die Integration des automatischen Theorembeweisers in den Beweisassistenten die Übersetzung von Aussagen in die Logik des automatischen Theorembeweisers und die Übersetzung von Beweisen in die Logik des Beweisassistenten. Um den Suchraum des automatischen Theorembeweisers einzuschränken, wird nur eine für die zu beweisende Aussage relevante Auswahl von Fakten übersetzt. Die Erfolgsquote der automatischen Beweissuche hängt ab von den verschiedenen Übersetzungen, der Auswahl von relevanten Fakten sowie von dem automatischen Theorembeweiser selbst.

Wir verbessern die Integration von automatischen Theorembeweisern in Beweisassistenten. Unter anderem lernen wir von vorhergegangenen Beweisen, relevante Fakten auszuwählen sowie Entscheidungen von automatischen Theorembeweisern zu beeinflussen. Weiters erstellen wir automatische Beweisübersetzungen für mehrere automatische Theorembeweiser, für die eine solche Übersetzung bisher nicht verfügbar war.

Unsere Arbeit erhöht die Erfolgsquote der Beweissuche in Beweisassistenten.

Abstract (English)

Proof assistants are programs that verify the correctness of formal proofs. They can increase the confidence in results from domains such as mathematics, informatics, physics, and philosophy. However, it requires extensive labour and expertise to write proofs accepted by proof assistants. In this thesis, we improve proof automation in proof assistants.

Automated theorem provers are programs that search for proofs automatically. Our goal is to find proofs in proof assistants using automated theorem provers. However, this is not directly possible when the logic of an automated theorem prover and that of a proof assistant differ.

In this case, the integration of the automated theorem prover into the proof assistant requires the translation of statements to the logic of the automated theorem prover and the translation of proofs to the logic of the proof assistant. To restrict the search space of the automated theorem prover, only a selection of facts relevant to the current conjecture is translated. The success rate of the automatic proof search in proof assistants depends on the various translations, the selection of relevant facts as well as on the automated theorem prover itself.

We improve the integration of automated theorem provers into proof assistants. Among others, we learn from previous proofs to select relevant facts as well as to guide automated theorem provers to make good decisions. Furthermore, we create automated proof translations for several automated theorem provers for which such a translation was not previously available.

Our work increases the success ratio of proof search in proof assistants.

Stats
The PDF-Document has been downloaded 10 times.