[ ] or SUCCESS is Not Enough: Current Technology and Future Directions in Proof Presentation
Johann M. Ph. Schumann, Peter Robinson, Daniel J. Clancy · 2001
Automated theorem provers for first order logic are now around for several decades. Over the last few years, their deductive power to solve hard problems has increased tremendously. The annual CASC system competitions [Se97] give a clear picture of this situation. However, today's automated theorem provers are restricted by general usability than by raw deductive power. As a result of this, there are only very few serious applications of automated theorem provers. There are numerous features which a theorem prover lacks for real-world applicability. An automated theorem prover (as it is currently seen) is nothing more than a fast and elaborate search procedure. In that sense, an ATP can compared to a formulated race car, cool and fast, but virtually unusable for shopping groceries around the corner. Many important features are missing, or are optimized for speed rather than for applicability. [Schol] identifies important features which are needed for practical usability like detection of non-theorems, handling of modal/inductive proof tasks, control of the prover, and proof output. In this paper, we will focus solely on the last point, the presentation of the ATP's result to the user. In the rest of this paper, we will first discuss the general importance of providing feedback to the user, then we will describe the system ExplainIt!, a part of the deductive synthesis system AMPHION/NAV. In the conclusions we will relate proof presentation to other ways of post-processing a proof found by an ATP and stress their role in the future of automated deduction.