Automated Theorem Proving on CoqGym (test)
30Success RateASTactic + hammer
Evaluation results
| Method | Links | |
|---|---|---|
| ASTactic + hammercombination=sequential use of hammer and ASTactic2019.05 | 30 | |
| hammertime limit=10 minutes2019.05 | 24.8 | |
| hammertime limit=20 seconds2019.05 | 17.8 | |
| ASTactic + autocombination=sequential use of auto and ASTactic2019.05 | 12.8 | |
| ASTacticbeam width=20, depth limit=502019.05 | 12.2 | |
| easy2019.05 | 4.9 | |
| intuition2019.05 | 4.4 | |
| auto2019.05 | 2.9 | |
| trivial2019.05 | 2.4 |