Conclusion
An Empirical Assessment
- 8 years of data from the TPTP World - 2015 to 2023
- 9 coherent SPC sets
- 6 evaluation measures
- Some noteworthy first solutions
- Stronger progress from v6.3.0 (2015) to v7.1.0 (2018)
- Period of quiet until v8.2.0 (2023)
- Some highlights
- The release of Waldmeister in 1997
- The release of Satallax 2.8 in 2015
- The release of Vampire 4.0.5 in 2016
- The release of Vampire 4.2 in 2017
- The release of iProver versions 2.5 and 2.8 in 2016 and 2018
- The release of Zipperposition 2.0 in 2020
- The release of SnakeForV 1.0 in 2022
- The monotonized ratings went down, but not dramatically
- The raw ratings were generally stable
- Contrast to the decreasing ratings from 2011 to 2016
- Possible causes
- Developers adding breadth at the expense of depth
- Top groups dominate the field and attract the best talent
- New systems' approaches that impact ratings
- Machine learning techniques focussed on homogeneous problem sets
- SMT solving absorbing effort
- The divisions of CASC
- CASC causing incremental development
- Stability modulo perturbations of the input
- Resource usage
- Verifiability of proofs/models
- Range of logics covered
- Ease of building and deploying
- Portability to different hardware and operating systems
- Availability of source code
- Quality of source code and its documentation
- Licensing
- User documentation
- Developer support (maybe most important!)