Faculty of Computer Science

Research Group Theoretical Computer Science

Oberseminar: Heterogene formale Methoden

Abstract:

Automated theorem proving aims to develop programs that are able to prove whether a given conjecture holds with respect to a given set of premises. In order to reduce the resulting computational complexity, methods from artificial intelligence and machine learning are applied, e.g. in order to decide which premises to choose or which proof strategies to use. In this talk I will present two selected talks from the 3rd Conference on Artificial Intelligence and Theorem Proving (AITP 2018):

Christoph Benzmüller and Dana Scott, Some Reflections on a Computer-aided Theory Exploration Study in Category Theory:
In this presentation I will show some benefits of automated theorem proving. The authors presented a the stepwise development of an axiomatization for category theory. Interestingly, this procedure was strongly guided by the use of several automated theorem provers and a model finder.

Bartosz Piotrowski and Josef Urban, ATP-guidance for Learning Premise Selection:
In order to prove your exercise conjectures from math class 101 you probably do not need every single theorem from the respective lecture but a rather small subset. The same holds for automated theorem provers. Thus, one might try to reduce the complexity of each proof attempt by selecting of those axioms that seem to be most beneficial for a specific conjecture. In this presentation I will present an approach to premise selection using XGBoost.