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.