TacticToe is a tactic-based theorem prover developed for HOL4.
It searches for a proof by repeatedly applying suitable tactics
to each new intermediate goal it produces.
- 2016: First version of TacticToe
- 2017: Integration in the HOL4 distribution
- 2018: Premise selection complements tactic selection
Experiments on the CakeML library
The current implementation of TacticToe is included
in the HOL4 distribution.
TacticToe on HOL4 goals.
Video of TacticToe proving a summation formula by induction.
|27/05/19||standard library (no let)||15s,ortho10,presel500,thm16||10824||5738 (53.0%)|