A view of automated proof checking and proving

Different techniques of automated formal reasoning are described and their performance and requirements on the human user are evaluated. The main trade-off is between autonomy and flexibility in conducting proofs. Examples of the use of techniques and existing systems are given, but no attempt of an exhaustive overview is made. The goal is to provide the reader with an idea of what to look for when selecting an approach for his/her application.