Abstract

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 HOLHammer strategy solves 32% in the same amount of
time.

BibTeX

@inproceedings{tgckju-lpar17,
 author    = {Thibault Gauthier and Cezary Kaliszyk and Josef Urban},
 title     = {{TacticToe}: Learning to Reason with {HOL4} Tactics},
 booktitle = {LPAR-21. 21st International Conference on Logic for
Programming, Artificial Intelligence and Reasoning},
 editor    = {Thomas Eiter and David Sands},
 series    = {EPiC Series in Computing},
 volume    = {46},
 pages     = {125--143},
 year      = {2017},
 publisher = {EasyChair},
 bibsource = {EasyChair, http://www.easychair.org},
 issn      = {2398-7340}}