Learning to Reason with HOL4 tactics
  Techniques combining machine learning with translation to automated reasoning
have recently become an important component of formal proof assistants. Such
"hammer" tech- niques complement traditional proof assistant automation as
implemented by tactics and decision procedures. In this paper we present a
unified proof assistant automation approach which attempts to automate the
selection of appropriate tactics and tactic-sequences com- bined with an
optimized small-scale hammering approach. We implement the technique as a
tactic-level automation for HOL4: TacticToe. It implements a modified
A*-algorithm directly in HOL4 that explores different tactic-level proof paths,
guiding their selection by learning from a large number of previous
tactic-level proofs. Unlike the existing hammer methods, TacticToe avoids
translation to FOL, working directly on the HOL level. By combining tactic
prediction and premise selection, TacticToe is able to re-prove 39 percent of
7902 HOL4 theorems in 5 seconds whereas the best single HOL(y)Hammer strategy
solves 32 percent in the same amount of time.
