ttt : tactic
STRUCTURE
tacticToe
SYNOPSIS
General purpose tactic relying on a automatic selection of tactics extracted from from human-written proof scripts. It returns an automatically generated proof script that solves the goal. A good practice is to replace the call of tacticToe.ttt by the generated proof script.
DESCRIPTION
Select relevant tactics and theorems for proving a goal using the k-nearest neighbor premise selection algorithm and relies on Monte Carlo tree search to expand multiple proof trees. In practice, this means that the intermediate goals created by better ranked tactics are explored more deeply.
FAILURE
Fails if the supplied goal does not contain boolean terms only. Or if the proof search saturates, it often happens when there is not enough recorded tactics. Or if no proof is found in less than a 15 seconds (default). This timeout can be modifed by tacticToe.set_timeout. Or if the proof fails to reconstruct.
EXAMPLE
- load "tttUnfold"; load "tacticToe"; open tacticToe;
(* output omitted *)
> val it = () : unit

- tttUnfold.ttt_record (); (* takes between 1 and 10 hours the first time it is called *)
(* output omitted *)
> val it = (): unit

- ttt ([],``1+1=2``);
Loading 3091 theorems 
Loading 12126 tactics
tactictoe found a proof:
  (SRW_TAC []) []
> val it = ([], fn): goal list * validation
COMMENTS
See src/tactictoe/README for more information on how to record the tactic data. See more examples in src/tactictoe/examples.
SEEALSO
tactictoe, hh
HOL  Kananaskis-13