Finding proofs and checking proofs

John Harrison.

To appear in the Proceedings of the ECAI-96 Workshop on Representation of mathematical knowledge.


The classic dichotomy between proof discovery and proof presentation resurfaces in automated deduction. The LCF style of theorem proving offers a promising way to integrate formal deductive proof with higher-level algorithmic or heuristic forms of mathematical activity. One way of dealing with the potential inefficiency of a reduction to a formal deductive system is to exploit the separation of proof finding and proof checking. This can be relevant both to the implementation difficulty of computer proof assistants, and the speed with which they run. Exploiting the separation makes it practical to use many of the usual algorithmic and heuristic approaches to mathematical problem-solving while maintaining the soundness of a formal deductive system. There is an interesting analogy with the NP and co-NP complexity classes.

DVI or PostScript.