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.
Demo of
TacticToe on HOL4 goals.
Video of
TacticToe proving a summation formula by induction.
| Date | Dataset | Parameters | Total | Proven |
|---|---|---|---|---|
| 27/05/19 | standard library (no let) | 15s,ortho10,presel500,thm16 | 10824 | 5738 (53.0%) |
|
3971206043e478ced916b0f9bfafd03a890441a4 |