Another point that has to be stressed is the distinction between automated deduction and computerated formal reasoning.
Why is this necessary? Well, because building proofs led along formal proofs is a rather creative activity, hence difficult to other automate. And it would be nice to have tools for achieving this.
Well, it happens that it is extremely difficult , but what is possible, what is feasible, is formal proof checking, because formal proof checking is a routine operation that can be very easily machine-checked. And although this sort of activity is very difficult for the human mind, because of the granularity of the logical stamps and proofs, this is something that machines can handle for us, can book keep very easily.
So what we are going to advocate is the use of semi-automated interactive proof assistance, and we will give also a brief introduction to the Coq.