Learned Provability Likelihood for Tactical Search
arXiv:2109.03234 · doi:10.4204/EPTCS.342.7
Abstract
We present a method to estimate the provability of a mathematical formula. We adapt the tactical theorem prover TacticToe to factor in these estimations. Experiments over the HOL4 library show an increase in the number of theorems re-proven by TacticToe thanks to this additional guidance. This amelioration in performance together with concurrent updates to the TacticToe framework lead to an improved user experience.
In Proceedings SCSS 2021, arXiv:2109.02501