Description of TacticToe


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.

Development Timeline

- 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.

Demos and presentations

Demo of TacticToe on HOL4 goals.
Video of TacticToe proving a summation formula by induction.

Results re-proving the HOL4 standard library

Date Dataset Parameters Total Proven
27/05/19 standard library (no let) 15s,ortho10,presel500,thm16 10824 5738 (53.0%)