Deduction as an Engineering Science

AbstractAlthough in recent years considerable progress has been made in the theory of automated theorem proving, the use of theorem provers in practice is still more or less restricted to a limited number of academic groups. A lot of effort has been spent in techniques to optimize the underlying logic engine by, for instance, developing efficient datastructures or controlling redundancy in large search spaces (see [29]). However, the development of techniques and methodologies to integrate such a logic engine into an overall proof assistant has gained less attention. In this paper we discuss the related research problems and will explore possible ways to tackle these problems