Experimenting with Machine Learning in Automatic Theorem Proving
First the notion of the heuristic and its importance for automatic theorem proving is explained. The question of how to construct a useful system of heuristics and notions is posed, and it is argued for the importance of learning. A simple example of learning a lemma is shown using the Inductive Logic Programming system Progol. Second a general framework for learning heuristics is discussed and the proof checking system Mizar providing a large body of mathematics is found suitable to learn upon. The process of modifying Mizar for use with Progol is shortly described, e.g. turning the mathematical texts to Prolog structures, creating initial notions, creating the initial base of rules from theorems and definitions, preparing proofs for learning, and problems with polymorphism. Finally first experiments in this environment are described, which include learning the notion of atomic formula and learning how to use initial rules in the proof of Rolle's theorem. This work was supported by Esprit Project 20237 Inductive Logic Programming II This article is an abridged version of the master thesis done under the guidence of doc. RNDr. Petr Stepanek, DrSc. at the Faculty of Mathematics and Physics of the Charles University