Progress in Automated Theorem Proving, 1997 - 1999
Abstract
Despite some impressive individual achievements, the extreme difficulty
of Automated Theorem Proving (ATP) means that progress in ATP is slow
relative to, e.g., some aspects of commercial information technology.
The (relatively) slow progress has two distinct disadvantages.
First, for the researchers, it is difficult to determine if a
direction of investigation is making a meaningful contribution.
Second, for unaware observers, a lack of progress leads to a loss of
interest and confidence in the field.
In this context it is important that progress in
ATP be measured, monitored, and recognized.
This paper presents quantitative measures that show progress in ATP,
from mid-1997 to the end of 1999.
The measures are based on collected performance data from ATP systems.