"TacticToe: Learning to Reason with HOL4 Tactics."

Thibault Gauthier, Cezary Kaliszyk, Josef Urban (2017)
a service of Schloss Dagstuhl - Leibniz Center for Informatics