John Harrison.
To appear in the Proceedings of the ECAI-96
Workshop on Representation of mathematical knowledge.
Abstract:
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.