Marco Ziener:
Mixing Automated Theorem Proving and Machine Learning
Kurzbeschreibung
Artificial Intelligence suffers a dichotomy between symbolic and numeric methods. With the advent of Deep Learning and the good performance on several different fields, its applications in context of the automated theorem prover Leo-III are explored. By applying methods from functional programming, this thesis introduces a reconstruction routine for proofs which allows to execute them and subject them for further analysis. Furthermore, the role of clause selection in internal proof-guidance is explored by modeling the proof process as a Markov Decision Process without clause selection and the application of a Markov Decision Process for optimizing the clause selection is described. In the end, further applications of machine learning techniques in Leo-III are outlined.