That formal proofs can establish elementary facts of arithmetic was demonstrated, if not before, by Principia Mathematica. Among many of those who are aware of the achievement, Principia Mathematica influences their apprehension of how hard it is to do arithmetic by proof.
As a response to the relatively poor mathematical abilities of modern proof tools (by comparison with tools for symbolic mathematics which do not produce proofs) some have sought to build proof tools on the more powerful though less sound foundations of a symbolic mathematics tool.
We draw together here some ideas on how proof tools might be engineered which are both sound and efficient in undertaking calculations and computations.
|what is a proof?|
|decision procedures||reflection principles|
|logic for problem solving||constraint programming|