Explaining Interactive Theorem Proving Tactic Prediction Using Inductive Logic Programming

This paper proposes a novel approach to improve tactic prediction in Interactive Theorem Provers (ITPs) by leveraging Inductive Logic Programming (ILP) to learn explainable rules for tactic selection, enhancing both the accuracy and interpretability of existing methods like k-NN.