Evaluation on the TPTP
- About the TPTP Problem Library
- Evaluated on all 1310 FOL problems with a conjecture and without equality
|
|
|
Problems
FOL
|
|
Trans'l
RM3
|
|
Truth Ev.
RM3
|
|
| FOL Theorems
|
| 987
|
| 508
|
| 158
|
| RM3 Non-thms
|
|
|
| 361
|
| 376
|
| FOL Non-theorems
|
| 323
|
| 223
|
| 158
|
| Total
|
| 1310
|
| 1092
|
| 692
|
- Interestingly ...
- 40 of the 1310 problems have rating 1.00 in the TPTP
33 FOL theorems, 7 FOL non-theorems
- The translational approach solved none of those 40
- The truth evaluation approach finds 15 to be RM3 non-theorems
13/33 FOL theorems, 2/7 FOL non-theorems