ttt
tacticToe.ttt : tactic
General purpose tactic relying on a automatic selection of tactics
extracted 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.
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 search saturates, this typically happens when there is not enough
recorded tactics. Or if the search times out. This timeout can be
modifed by tacticToe.set_timeout. Or if the proof fails to
reconstruct.
Example
- load "tttUnfold"; load "tacticToe"; open tacticToe;
- tttUnfold.ttt_record (); (* takes multiple hours the first time it is called *)
- ttt ([],``1+1=2``);
Comments
See src/tactictoe/README for more information on how to record the
tactic data. See more examples in src/tactictoe/examples.