TacticToe: learning to reason with HOL4 tactics. (English) Zbl 1403.68224

Eiter, Thomas (ed.) et al., LPAR-21. 21st international conference on logic for programming, artificial intelligence and reasoning, Maun, Botswana, May 8–12, 2017. Selected papers. Manchester: EasyChair. EPiC Series in Computing 46, 15-143 (2017).
Summary: Techniques combining machine learning with translation to automated reasoning have recently become an important component of formal proof assistants. Such “hammer” techniques 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 combined 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\%\) of 7902 HOL4 theorems in 5 seconds whereas the best single HOL(y)Hammer strategy solves \(32\%\) in the same amount of time.
For the entire collection see [Zbl 1398.68026].


68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T05 Learning and adaptive systems in artificial intelligence
Full Text: DOI arXiv